From 4243bd3e2a2285a83d1266fca76f9e997f278371 Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Sun, 10 Feb 2019 15:55:41 -0800
Subject: [PATCH] a bug fix in simple sign lemma

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

diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index c30e409b0..9fbbdfd8b 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -2312,7 +2312,7 @@ struct solver::imp {
             }
         }
         mk_ineq(m.var(), (sign.is_pos()? llc::GT : llc ::LT), current_lemma());
-		TRACE("nla_solver", print_lemma_and_expl(tout););
+        TRACE("nla_solver", print_lemma_and_expl(tout););
     }
 
     bool generate_simple_tangent_lemma(const rooted_mon* rm) {
@@ -2325,7 +2325,7 @@ struct solver::imp {
         SASSERT(!mv.is_zero() && !v.is_zero());
         rational sign = rational(rat_sign(mv));
         if (sign != rat_sign(v)) {
-            generate_simple_sign_lemma(sign, m);
+            generate_simple_sign_lemma(-sign, m);
             return true;
         }
         bool gt = abs(mv) > abs(v);