necto wrote: > That being said, do we know how exactly the unstable addresses result in > unstable results?
One mechanism that we studied in the past weeks is the SMT issue refutation: assertion order is that of the constraint order in the `ConstraintMap`, and it turns out Z3 runs a query differently depending on the order of the assertions. There are likely other mechanisms, for example, the SymbolRef `EquivalenceClass` in RangeConstraintManager is an `ImmutableMap<SymbolRef, ...>`. With different ordering, the constraint manager might choose a different representative `SymbolRef` for a given class. This is speculative, though. > By the way, the Python language (where performance is not prioritized) rules > out these subtle bugs by recording the order of insertion within its `dict` > (associative map) datatype and using that as the iteration order. Interesting parallel, as this patch is applying the same strategy for SymbolRef maps https://github.com/llvm/llvm-project/pull/121551 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
