mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-14 04:41:48 +00:00
Code Activity

Merge f39e462534 into 83b60990b1

Browse source
This commit is contained in:
Copilot 2026-02-12 23:02:32 -08:00 • committed by GitHub
commit 306f554057
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 14 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/smt_model_finder.cpp
View file

@ -2559,13 +2559,21 @@ namespace smt {
ptr_buffer<expr> eqs;
for (auto const& kv : inv) {
expr* val = kv.m_key;
eqs.push_back(m.mk_eq(sk, val));
// When quantifiers are flattened, the instantiation set may contain
// values from nested quantifiers with incompatible sorts. Only create
// equality constraints when sorts match to avoid well-sortedness violations.
if (sk->get_sort() == val->get_sort()) {
eqs.push_back(m.mk_eq(sk, val));
}
}
// Only assert a constraint if we have at least one valid equality
if (!eqs.empty()) {
expr_ref new_cnstr(m);
new_cnstr = m.mk_or(eqs);
TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";);
aux_ctx->assert_expr(new_cnstr);
asserted_something = true;
}
expr_ref new_cnstr(m);
new_cnstr = m.mk_or(eqs);
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;
}