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

Improve comment explaining sort check fix

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:35:49 +00:00
parent 8d47a9dc61
commit 2193e04f67
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_model_finder.cpp
View file

@ -2559,7 +2559,9 @@ namespace smt {
ptr_buffer<expr> eqs; ptr_buffer<expr> eqs;
for (auto const& kv : inv) { for (auto const& kv : inv) {
expr* val = kv.m_key; expr* val = kv.m_key;
// Only create equality if sorts match // 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()) { if (sk->get_sort() == val->get_sort()) {
eqs.push_back(m.mk_eq(sk, val)); eqs.push_back(m.mk_eq(sk, val));
} }