mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fixes in get_lower,get_upper of theory_lra

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-06-29 14:38:10 -07:00
parent 342feeff03
commit 4d88818560
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_lra.cpp
View file

@ -2613,10 +2613,13 @@ public:
bool get_lower(enode* n, expr_ref& r) {
theory_var v = n->get_th_var(get_id());
if (!can_get_value(v))
return false;
lp::var_index vi = m_theory_var2var_index[v];
lp::constraint_index ci;
rational val;
bool is_strict;
if (m_solver->has_lower_bound(v, ci, val, is_strict)) {
if (m_solver->has_lower_bound(vi, ci, val, is_strict)) {
r = a.mk_numeral(val, is_int(n));
return true;
}
@ -2625,10 +2628,13 @@ public:
bool get_upper(enode* n, expr_ref& r) {
theory_var v = n->get_th_var(get_id());
if (!can_get_value(v))
return false;
lp::var_index vi = m_theory_var2var_index[v];
lp::constraint_index ci;
rational val;
bool is_strict;
if (m_solver->has_upper_bound(v, ci, val, is_strict)) {
if (m_solver->has_upper_bound(vi, ci, val, is_strict)) {
r = a.mk_numeral(val, is_int(n));
return true;
}