From 88f4ce68fd46b2200c9d75d568eded5accc4c27f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 13 Jul 2018 13:51:07 -0700
Subject: [PATCH] fix model generation regression exposed in nightly builds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_lra.cpp | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ff5b72159..9c054830c 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1118,7 +1118,7 @@ public:
(v != null_theory_var) &&
(v < static_cast<theory_var>(m_theory_var2var_index.size())) &&
(UINT_MAX != m_theory_var2var_index[v]) &&
- !m_variable_values.empty();
+ (!m_variable_values.empty() || m_solver->is_term(m_theory_var2var_index[v]));
}
bool can_get_bound(theory_var v) const {
@@ -1163,13 +1163,19 @@ public:
}
rational get_value(theory_var v) const {
- if (!can_get_value(v)) return rational::zero();
+
+ if (v == null_theory_var ||
+ v >= static_cast<theory_var>(m_theory_var2var_index.size()))
+ return rational::zero();
+
lp::var_index vi = m_theory_var2var_index[v];
if (m_variable_values.count(vi) > 0)
return m_variable_values[vi];
- if(!m_solver->is_term(vi))
+ if (!m_solver->is_term(vi)) {
+ TRACE("arith", tout << "not a term v" << v << "\n";);
return rational::zero();
+ }
m_todo_terms.push_back(std::make_pair(vi, rational::one()));
rational result(0);