mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

use lar_solver directly to compare variable values in assume_eqs()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-02-20 10:36:13 -08:00
parent 6549984dd4
commit c0b49e95c4
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_lra.cpp
View file

@ -341,7 +341,7 @@ class theory_lra::imp {
return m_th.is_int(v);
}
else {
return (unsigned)std::hash<lp::mpq>()(m_th.get_value(v));
return (unsigned)std::hash<lp::impq>()(m_th.get_ivalue(v));
}
}
};
@ -1652,7 +1652,7 @@ public:
if (!th.is_relevant_and_shared(n1)) {
continue;
}
if (!can_get_value(v)) {
if (!can_get_ivalue(v)) {
continue;
}
theory_var other = m_model_eqs.insert_if_not_there(v);
@ -1705,7 +1705,7 @@ public:
return m_nra->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2));
}
else {
return get_value(v1) == get_value(v2);
return get_ivalue(v1) == get_ivalue(v2);
}
}