From 4d888185608e3a03c32d0c96005d91edd5011553 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 29 Jun 2018 14:38:10 -0700 Subject: [PATCH] fixes in get_lower,get_upper of theory_lra Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 120ce1517..513248d4b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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; }