From 2bab591ef3e0e5f56d3ed3ea8c1152781746b95c Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 8 Feb 2019 16:51:53 -0800
Subject: [PATCH] restore qfnia_tactic.cpp to expose a bug

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

diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index ef23dd327..6a1a37aa8 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -2292,6 +2292,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););
     }
 
     bool generate_simple_tangent_lemma(const rooted_mon* rm) {