necto wrote: > At which point do you expect it to simplify the symbolic expression?
Digging a little deeper with the help of Claude Opus, I think I discovered the root issue here. I cite it verbatim as it checks out. Opus: > 1. assumeSym (line 26) calls Sym = simplify(State, S1 & 8). > 2. Inside simplify, simplifyToSVal → SValBuilder::simplifySVal performs the > exact substitution you'd expect: S1 is pinned to the > concrete 2, so S1 & 8 folds all the way to the concrete integer 0 > (nonloc::ConcreteInt). This is the same machinery the C++ > cast uses — and it works here too. > 3. But simplify's return type is SymbolRef. It only keeps the simplified > result if (SimplifiedVal.getAsSymbol()). A ConcreteInt > has no underlying symbol, so getAsSymbol() returns null. > 4. So simplify discards the folded 0 and returns the original, unsimplified > symbol S1 & 8. https://github.com/llvm/llvm-project/pull/210912 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
