necto wrote: > I'll try to use `simplifyToSVal` in the 3 places `simplify` is used in and > handle concrete values there
I removed the `simplify` wrapper and inlined it in the 3 places where it was used. You can see the effect in the commit history: - 934cd3ccc7fd Revert "Fix PthreadLockChecker" - remove the sympomatic fix - 1ae1e1dc5b8d Add a test case demonstrating missed simplification demonstrate the imprecision introduced by `simplify`. Note that the imprecision is masked in the third case (`assumeSymUnsupported`), but it still leads to some wasted work. - dcb89e17978a Fix the simplification blind spot for concrete integers Implement a proper minimal fix. It also made the z3-refutation test moot because it relied on this imprecision to demonstrate the difference z3 brings. It is a further proof that this fix reduces number of infeasible paths we explore. - 96bdb09b678a Restore meaningful z3-crosscheck.c test Z3 is still useful, so I let Claude find another approximation point of the range constraint manager compared to Z3. It is likely there is more simplification that could be done, but I wanted to keep the fix scope narrow to avoid regression risks. How does it look, @steakhal ? https://github.com/llvm/llvm-project/pull/210912 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
