steakhal wrote: The tests look really fragile. Without knowing exactly how did we end up with a SymExpr that fails to convert to a Z3 formula, I'm tempted to push back. I think I've seen similar conversion errors and fixes from you. This suggests to me that we need to understand the underlying reasons why we have these SymExprs and systematically solve these issues.
My gut instincts suggests that this SymExpr lacks some SymbolCast (due to the inappropriate modeling of casts), which bites back here as well. If that's the case, we could provide a translation layer that would visit a SymExpr and output a valid SymExpr that has the bit-widening/truncating SymbolCasts where needed. That way only Z3 would have a different "view" of these symbols while the engine could still have the wrong SymExprs. The added benefit would be to have a centralized place of the hacks that we currently embed into the Z3 expr converter. https://github.com/llvm/llvm-project/pull/158276 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
