From 7cd901019f38c5cf3fdd68e323fed3293704a20a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 5 Jun 2021 17:14:51 -0700
Subject: [PATCH] #5324

---
 src/math/simplex/model_based_opt.cpp | 11 +++++++++--
 src/math/simplex/model_based_opt.h   |  2 ++
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index a52dabf9e..32b957348 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -166,7 +166,7 @@ namespace opt {
         return true;
     }
 
-#define PASSERT(_e_) if (!(_e_)) { TRACE("opt1", display(tout, r); display(tout);); SASSERT(_e_); }
+#define PASSERT(_e_) { CTRACE("qe", !(_e_), display(tout, r); display(tout);); SASSERT(_e_); }
 
     bool model_based_opt::invariant(unsigned index, row const& r) {
         vector<var> const& vars = r.m_vars;
@@ -423,6 +423,13 @@ namespace opt {
         }
         return val;
     }    
+
+    rational model_based_opt::eval(vector<var> const& coeffs) const {
+        rational val(0);
+        for (var const& v : coeffs) 
+            val += v.m_coeff * eval(v.m_id);
+        return val;
+    }
  
     rational model_based_opt::get_coefficient(unsigned row_id, unsigned var_id) const {
         return m_rows[row_id].get_coefficient(var_id);
@@ -1193,7 +1200,7 @@ namespace opt {
             row& r1 = m_rows[row_id1];
             vector<var> coeffs;
             mk_coeffs_without(coeffs, r1.m_vars, x);
-            rational c = r1.m_coeff;
+            rational c = mod(-eval(coeffs), a);
             add_divides(coeffs, c, a);
         }
         unsigned_vector const& row_ids = m_var2row_ids[x];
diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h
index 047f03cc4..bb6f8f91c 100644
--- a/src/math/simplex/model_based_opt.h
+++ b/src/math/simplex/model_based_opt.h
@@ -104,6 +104,8 @@ namespace opt {
         rational eval(unsigned x) const;
         
         rational eval(def const& d) const;
+        
+        rational eval(vector<var> const& coeffs) const;
 
         void resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x);