From d1a5635b4ad7f8632356b380f3a9b1fc83fdb04f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 6 Mar 2019 15:11:13 +1400
Subject: [PATCH] better model based lemmaas

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

diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 4e987ce7c..851bfef18 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -958,13 +958,14 @@ struct solver::imp {
             int product_sign = rat_sign(m);
             if (mon_sign != product_sign) {
                 basic_sign_lemma_model_based_one_mon(m, product_sign);
-                return true;
+                if (done())
+                    return true;
             }
             i++;
             if (i == m_to_refine.size())
                 i = 0;
         } while (i != ii);
-        return false;
+        return m_lemma_vec->size() > 0;
     }