From c4416f822eaeb63e6052b4bf287ded86bc7a4875 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 1 Apr 2020 10:44:15 -0700
Subject: [PATCH] add an assert

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_core.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 28d3d2277..a8ef61990 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1374,6 +1374,7 @@ void core::patch_monomial_with_real_var(lpvar j) {
     if (!var_is_int(j)  &&
         !var_is_used_in_a_correct_monic(j)
         &&  try_to_patch(j, v)) {
+        SASSERT(v == val(j));
         m_to_refine.erase(j);
     } else {
         rational r = val(j) / v;
@@ -1383,6 +1384,7 @@ void core::patch_monomial_with_real_var(lpvar j) {
                 continue;
             if (try_to_patch(k, r * val(k))) { // r * val(k) gives the right value of k
                 m_to_refine.erase(j);
+                SASSERT(mul_val(m) == val(j));
                 break;
             }
         }