================
@@ -75,16 +75,28 @@ void
Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
for (const auto &[Sym, Range] : Constraints) {
auto RangeIt = Range.begin();
- llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
+ std::optional<llvm::SMTExprRef> SMTConstraintsOpt = SMTConv::getRangeExpr(
RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
/*InRange=*/true);
+ if (!SMTConstraintsOpt) {
+ continue;
+ }
+ auto SMTConstraints = SMTConstraintsOpt.value();
+ bool ShouldAddConstraint = true;
while ((++RangeIt) != Range.end()) {
- SMTConstraints = RefutationSolver->mkOr(
- SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
- RangeIt->From(), RangeIt->To(),
- /*InRange=*/true));
+ std::optional<llvm::SMTExprRef> ConstraintOpt = SMTConv::getRangeExpr(
+ RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
+ /*InRange=*/true);
+ if (!ConstraintOpt) {
+ ShouldAddConstraint = false;
+ break;
+ }
+ SMTConstraints =
+ RefutationSolver->mkOr(SMTConstraints, ConstraintOpt.value());
+ }
+ if (ShouldAddConstraint) {
+ RefutationSolver->addConstraint(SMTConstraints);
}
- RefutationSolver->addConstraint(SMTConstraints);
----------------
rdevshp wrote:
I have switched to letting it crash instead.
https://github.com/llvm/llvm-project/pull/205078
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
