mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

fix ordering of delayed assume eqs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-26 16:24:34 -07:00
parent 7a04e52c41
commit 12f62e73d5
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_lra.cpp
View file

@ -1583,7 +1583,7 @@ public:
} }
tout << "\n"; ); tout << "\n"; );
if (!m_use_nra_model && !m_nla) { if (!m_use_nra_model && !m_nla) {
// lp().random_update(vars.size(), vars.c_ptr()); lp().random_update(vars.size(), vars.c_ptr());
} }
m_model_eqs.reset(); m_model_eqs.reset();
TRACE("arith", display(tout);); TRACE("arith", display(tout););
@ -1611,6 +1611,7 @@ public:
tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n"; tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
tout << "v" << v << " = " << "v" << other << "\n";); tout << "v" << v << " = " << "v" << other << "\n";);
m_assume_eq_candidates.push_back(std::make_pair(v, other)); m_assume_eq_candidates.push_back(std::make_pair(v, other));
num_candidates++;
} }
} }