diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 6d1d4b2cc..d6d035454 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -640,16 +640,6 @@ namespace nlsat {
 
         literal mk_ineq_literal(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even) {
             SASSERT(k == atom::LT || k == atom::GT || k == atom::EQ);
-            if (sz == 0) {
-                switch (k) {
-                case atom::LT: return false_literal;  // 0 < 0
-                case atom::EQ: return true_literal;   // 0 == 0
-                case atom::GT: return false_literal;  // 0 > 0
-                default: 
-                    UNREACHABLE();
-                    return null_literal;
-                }
-            }
             bool is_const = true;
             polynomial::manager::scoped_numeral cnst(m_pm.m());
             m_pm.m().set(cnst, 1);
@@ -2657,6 +2647,7 @@ namespace nlsat {
                 for (clause* c : m_clauses) {
                     if (solve_var(*c, v, p, q)) {
                         q = -q;
+                        TRACE("nlsat", tout << "p: " << p << "\nq: " << q << "\n x" << v << "\n";);
                         m_patch_var.push_back(v);
                         m_patch_num.push_back(q);
                         m_patch_denom.push_back(p);
@@ -2698,6 +2689,8 @@ namespace nlsat {
             u_map<literal> b2l;
             scoped_literal_vector lits(m_solver);
             svector<bool> even;
+            polynomial::manager::scoped_numeral cnst(m_pm.m());
+            m_pm.m().set(cnst, 1);
             unsigned num_atoms = m_atoms.size();
             for (unsigned j = 0; j < num_atoms; ++j) {
                 atom* a = m_atoms[j];
@@ -2712,9 +2705,12 @@ namespace nlsat {
                         poly * po = a1.p(i);
                         m_pm.substitute(po, x, q, p, pr);
                         change |= pr != po;
+                        TRACE("nlsat", tout << pr << "\n";);
                         if (m_pm.is_zero(pr)) {
                             ps.reset();
                             even.reset();
+                            even.push_back(false);
+                            ps.push_back(pr);
                             break;
                         }
                         if (m_pm.is_const(pr)) {
diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp
index f3f984e28..5016c951b 100644
--- a/src/nlsat/tactic/nlsat_tactic.cpp
+++ b/src/nlsat/tactic/nlsat_tactic.cpp
@@ -83,7 +83,7 @@ class nlsat_tactic : public tactic {
         bool eval_model(model& model, goal& g) {
             unsigned sz = g.size();
             for (unsigned i = 0; i < sz; i++) {
-                if (!model.is_true(g.form(i))) {
+                if (model.is_false(g.form(i))) {
                     TRACE("nlsat", tout << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";);
                     IF_VERBOSE(0, verbose_stream() << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";);
                     IF_VERBOSE(1, verbose_stream() << model << "\n");
@@ -152,12 +152,12 @@ class nlsat_tactic : public tactic {
             m_display_var.m_var2expr.reset();
             t2x.mk_inv(m_display_var.m_var2expr);
             m_solver.set_display_var(m_display_var);
-            
+            TRACE("nlsat", m_solver.display(tout););
             IF_VERBOSE(10000, m_solver.display(verbose_stream()));
             IF_VERBOSE(10000, g->display(verbose_stream()));
 
+
             lbool st = m_solver.check();
-           
             if (st == l_undef) {
             }
             else if (st == l_true) {
@@ -176,7 +176,7 @@ class nlsat_tactic : public tactic {
                     }
                 }
             }
-            else {
+            else if (st == l_false) {
                 expr_dependency* lcore = nullptr;
                 if (g->unsat_core_enabled()) {
                     vector<nlsat::assumption, false> assumptions;
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 684facd1c..f4d2f2b38 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -867,8 +867,8 @@ class solve_eqs_tactic : public tactic {
             expr_dependency_ref new_dep(m());
             for (app * v : m_ordered_vars) {
                 checkpoint();
-				expr_ref new_def(m());
-				proof_ref new_pr(m());
+                expr_ref new_def(m());
+                proof_ref new_pr(m());
                 expr * def = nullptr;
                 proof * pr = nullptr;
                 expr_dependency * dep = nullptr;