mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

decouple random update with assume eqs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-09 14:01:34 -07:00
parent 5ced73afb5
commit cd98a21984
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_lra.cpp
View file

@ -1586,6 +1586,9 @@ public:
} }
void random_update() { void random_update() {
if (m_use_nra_model || m_nla)
return;
m_model_eqs.reset(); m_model_eqs.reset();
svector<lpvar> vars; svector<lpvar> vars;
theory_var sz = static_cast<theory_var>(th.get_num_vars()); theory_var sz = static_cast<theory_var>(th.get_num_vars());
@ -1625,7 +1628,7 @@ public:
} }
} }
tout << "\n"; ); tout << "\n"; );
if (!vars.empty() && !m_use_nra_model && !m_nla) { if (!vars.empty()) {
lp().random_update(vars.size(), vars.c_ptr()); lp().random_update(vars.size(), vars.c_ptr());
} }
} }