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

Fix sort error with nested quantifiers by adding sort check

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:30:02 +00:00
parent 472ac6a97a
commit 8d47a9dc61
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_model_finder.cpp
View file

@ -2559,7 +2559,10 @@ 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;
eqs.push_back(m.mk_eq(sk, val)); // Only create equality if sorts match
if (sk->get_sort() == val->get_sort()) {
eqs.push_back(m.mk_eq(sk, val));
}
} }
expr_ref new_cnstr(m); expr_ref new_cnstr(m);
new_cnstr = m.mk_or(eqs); new_cnstr = m.mk_or(eqs);