mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-06 09:00:52 +00:00
Code Activity

Add check for empty equality list to prevent asserting false

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-12 15:37:28 +00:00
parent 2193e04f67
commit f39e462534
1 changed files with 8 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/smt_model_finder.cpp
View file

@ -2566,11 +2566,14 @@ namespace smt {
eqs.push_back(m.mk_eq(sk, val)); eqs.push_back(m.mk_eq(sk, val));
} }
} }
expr_ref new_cnstr(m); // Only assert a constraint if we have at least one valid equality
new_cnstr = m.mk_or(eqs); if (!eqs.empty()) {
TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";); expr_ref new_cnstr(m);
aux_ctx->assert_expr(new_cnstr); new_cnstr = m.mk_or(eqs);
asserted_something = true; TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";);
aux_ctx->assert_expr(new_cnstr);
asserted_something = true;
}
} }
return asserted_something; return asserted_something;
} }