From e683f4be21db3f2dd274011fb34ce9496dd07e1b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 12 Oct 2020 10:35:33 -0700
Subject: [PATCH] #4525 regression in model generation

---
 src/smt/theory_lra.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index d9323d433..4e158534d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1565,9 +1565,10 @@ public:
         if (m_variable_values.count(t.index()) > 0)
             return m_variable_values[t.index()];
         
-        if (!t.is_term()) {
+        if (!t.is_term() && lp().is_fixed(t.id())) 
+            return lp().column_lower_bound(t.id()).x;
+        if (!t.is_term()) 
             return rational::zero();
-        }
         
         m_todo_terms.push_back(std::make_pair(t, rational::one()));
         rational result(0);