From ca8f914dd886ada1def33b7e8a5772e33d8fd5cc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 21 Jul 2021 07:22:05 -0700
Subject: [PATCH] #5422

---
 src/math/simplex/model_based_opt.cpp | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 429a97ae2..5bc0b1836 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -134,7 +134,15 @@ namespace opt {
     }
 
     void model_based_opt::def::normalize() {
-        SASSERT(m_div.is_int());
+        if (!m_div.is_int()) {
+            rational den = denominator(m_div);
+            SASSERT(den > 1);
+            for (var& v : m_vars)
+                v.m_coeff *= den;
+            m_coeff *= den;
+            m_div *= den;
+
+        }
         if (m_div.is_neg()) {
             for (var& v : m_vars)
                 v.m_coeff.neg();
@@ -1249,6 +1257,7 @@ namespace opt {
         }
         def result;
         if (compute_def) {
+            TRACE("opt1", tout << m_rows[row_id1] << "\n";);
             result = def(m_rows[row_id1], x);
             m_var2value[x] = eval(result);
             TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);