From 9afc59d5b45fc7f22f192e7105f4701ed1f5ce80 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Jun 2021 15:39:23 -0700
Subject: [PATCH] #5324

---
 src/math/simplex/model_based_opt.cpp | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 32b957348..e383a39fd 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -1009,8 +1009,7 @@ namespace opt {
                     result = solve_for(glb_index, x, true);                
                 }
                 else {
-                    result = def();
-                    m_var2value[x] = rational::zero();
+                    result = def() + m_var2value[x];
                 }
                 SASSERT(eval(result) == eval(x));
             }
@@ -1130,9 +1129,8 @@ namespace opt {
         }
         TRACE("opt1", display(tout << "tableau after replace x by y := v" << y << "\n"););
         def result = project(y, compute_def);
-        if (compute_def) {
+        if (compute_def) 
             result = (result * D) + u;     
-        }
         SASSERT(!compute_def || eval(result) == eval(x));
         return result;
     }