From 905282ffe4ec675d96d80a059ede62815b2a790a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 5 Jul 2018 14:47:05 -0700 Subject: [PATCH] fix in theory_lra.cpp get_value Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 6b8d7a47d..b4415264b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1168,7 +1168,9 @@ public: if (m_variable_values.count(vi) > 0) return m_variable_values[vi]; - SASSERT (m_solver->is_term(vi)); + if(!m_solver->is_term(vi)) + return rational::zero(); + m_todo_terms.push_back(std::make_pair(vi, rational::one())); rational result(0); while (!m_todo_terms.empty()) {