vabridgers 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.
Hi @steakhal , thanks for the comment. I agree there could be some deeper issue here, but my immediate concern is to avoid the crash. Is it ok if we separate those concerns and first come up with a way to avoid the crash, then follow up with understanding and fixing the deeper concern? I admit I do not understand the details of SymExprs, but I needed to get attention on this new issue - hence this PR as a starting point. https://github.com/llvm/llvm-project/pull/158276 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
