mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

do not call get_model() from assume_eqs()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-02-15 22:08:08 -08:00
parent 0db112ef8f
commit c469ea2717
1 changed files with 3 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/smt/theory_lra.cpp
View file

@ -1620,23 +1620,6 @@ public:
m_variable_values.clear();
}
bool influences_nl_var(theory_var v) const {
return m_nla && m_nla->influences_nl_var(get_lpvar(v));
}
bool can_be_used_in_random_update(theory_var v) const {
if (!th.is_relevant_and_shared(get_enode(v)))
return false;
if (is_int(v))
return false;
if (influences_nl_var(v))
return false;
return true;
}
bool assume_eqs() {
svector<lpvar> vars;
theory_var sz = static_cast<theory_var>(th.get_num_vars());
@ -1647,10 +1630,6 @@ public:
if (vars.empty()) {
return false;
}
if (!m_use_nra_model) {
lp().random_update(vars.size(), vars.c_ptr());
}
init_variable_values();
TRACE("arith",
for (theory_var v = 0; v < sz; ++v) {
if (th.is_relevant_and_shared(get_enode(v))) {
@ -1658,6 +1637,9 @@ public:
}
}
tout << "\n"; );
if (!m_use_nra_model && !m_nla) {
lp().random_update(vars.size(), vars.c_ptr());
}
m_model_eqs.reset();
TRACE("arith", display(tout););