diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index a1bf8958b..d394c8d07 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -1625,6 +1625,7 @@ bool core::find_bfc_to_refine(const monomial* & m, factorization & bf){
 }
 
 void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) {
+    add_empty_lemma();
     SASSERT(sign == nla::rat_sign(product_value(m.vars())));
     for (lpvar j : m.vars()) {
         if (val(j).is_pos()) {
diff --git a/src/util/lp/nla_tangent_lemmas.cpp b/src/util/lp/nla_tangent_lemmas.cpp
index 5d0dc072a..17128ae26 100644
--- a/src/util/lp/nla_tangent_lemmas.cpp
+++ b/src/util/lp/nla_tangent_lemmas.cpp
@@ -104,7 +104,6 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) {
     if (m.size() != 2)
         return;
     TRACE("nla_solver", tout << "m:" << pp_mon(c(), m) << std::endl;);
-    c().add_empty_lemma();
     const rational v = c().product_value(m.vars());
     const rational mv = val(m);
     SASSERT(mv != v);
@@ -115,6 +114,7 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) {
         return;
     }
     /*
+    c().add_empty_lemma();
     bool gt = abs(mv) > abs(v);
     if (gt) {
         for (lpvar j : m.vars()) {