diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index dd6550080..5041ae2ed 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -6,6 +6,7 @@
 #include <map>
 #include <algorithm>
 #include "math/polynomial/algebraic_numbers.h"
+#include "nlsat_pp.h"
 namespace nlsat {
 
 // Local enums reused from previous scaffolding
@@ -40,8 +41,8 @@ namespace nlsat {
         solver& m_solver;
         polynomial_ref_vector const& m_P;
         var                          m_n;
-        assignment const&            m_s;
-            pmanager&                    m_pm;
+        assignment const&            sample() { return m_solver.get_assignment();}
+        pmanager&                    m_pm;
         anum_manager&                m_am;
         std::vector<property>        m_Q; // the set of properties to prove as in single_cell
         bool                         m_fail = false;
@@ -53,7 +54,8 @@ namespace nlsat {
         std::vector<std::vector<bool>> m_prop_dom;
         // max_x plays the role of n in algorith 1 of the levelwise paper.
         impl(solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am)
-            : m_solver(solver), m_P(ps), m_n(max_x), m_s(s), m_pm(pm), m_am(am) {
+            : m_solver(solver), m_P(ps), m_n(max_x),  m_pm(pm), m_am(am) {
+            TRACE(levelwise, tout  << "m_n:" << m_n << "\n";);    
             init_relation();
         }
 
@@ -115,9 +117,13 @@ namespace nlsat {
         }
         std::vector<property> seed_properties() {
             std::vector<property> Q;
+
             // Algorithm 1: initial goals are sgn_inv(p, s) for p in ps at current level of max_x
             for (unsigned i = 0; i < m_P.size(); ++i) {
                 poly* p = m_P.get(i);
+                TRACE(levelwise, display(tout << "p:", m_solver, polynomial_ref(p, m_pm)) << std::endl;
+                      tout << "max_var:" << m_pm.max_var(p) << std::endl;
+                      m_solver.display_assignment(tout << "sample()") << std::endl;);
                 Q.push_back(property{ prop_enum::sgn_inv_irreducible, p, /*s_idx*/0, /* level */ m_n});
             }
             return Q;
@@ -177,8 +183,8 @@ namespace nlsat {
 
         ::sign sign(poly * p) {
             polynomial_ref pr(p, m_P.m());
-            auto s = m_am.eval_sign_at(pr, m_s);
-            TRACE(nlsat_explain, tout << "p: " << p << " var: " << m_pm.max_var(p) << " sign: " << s << "\n";);
+            auto s = m_am.eval_sign_at(pr, sample());
+            TRACE(levelwise, tout << "p: " << p << " var: " << m_pm.max_var(p) << " sign: " << s << "\n";);
             return s;
         }
         result_struct construct_interval() {
@@ -206,7 +212,7 @@ namespace nlsat {
             
             std::vector<const poly*> p_non_null;
             for (const auto & pr: m_Q) {
-                if (pr.prop == prop_enum::sgn_inv_irreducible && sign(pr.p) != 0)
+                if (pr.prop == prop_enum::sgn_inv_irreducible && m_pm.max_var(pr.p) < m_i && sign(pr.p) != 0)
                     p_non_null.push_back(pr.p);
             }
             
diff --git a/src/nlsat/nlsat_pp.h b/src/nlsat/nlsat_pp.h
index f01a33215..4b86d775a 100644
--- a/src/nlsat/nlsat_pp.h
+++ b/src/nlsat/nlsat_pp.h
@@ -14,7 +14,7 @@ Abstract:
 #pragma once
 
 #include "nlsat/nlsat_solver.h"
-
+#include "nlsat/nlsat_scoped_literal_vector.h"
 namespace nlsat {
 
 inline std::ostream& display(std::ostream& out, pmanager& pm, polynomial_ref const& p, display_var_proc const& proc) {
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 97cac90fc..56a2f3a9e 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -39,6 +39,7 @@ Revision History:
 #include "nlsat/nlsat_simplify.h"
 #include "nlsat/nlsat_simple_checker.h"
 #include "nlsat/nlsat_variable_ordering_strategy.h"
+#include "nlsat_solver.h"
 
 #define NLSAT_EXTRA_VERBOSE
 
@@ -4123,10 +4124,14 @@ namespace nlsat {
         nlsat_params::collect_param_descrs(d);
     }
 
-    unsynch_mpq_manager & solver::qm() {
+    const assignment &solver::get_assignment() const {
+        return m_imp->m_assignment;
+    }
+    unsynch_mpq_manager &solver::qm()
+    {
         return m_imp->m_qm;
     }
-        
+
     anum_manager & solver::am() {
         return m_imp->m_am;
     }
diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
index ae403fc83..611b20ea7 100644
--- a/src/nlsat/nlsat_solver.h
+++ b/src/nlsat/nlsat_solver.h
@@ -244,7 +244,7 @@ namespace nlsat {
         // -----------------------
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
-
+        const assignment& get_assignment() const; 
         void reset();
         void collect_statistics(statistics & st);
         void reset_statistics();
@@ -294,7 +294,7 @@ namespace nlsat {
         std::ostream& display_assignment(std::ostream& out) const;
 
         std::ostream& display_var(std::ostream& out, unsigned j) const;
-        
+
     };
 
 };
diff --git a/src/util/trace_tags.def b/src/util/trace_tags.def
index ffa631d7a..96ce0d5bf 100644
--- a/src/util/trace_tags.def
+++ b/src/util/trace_tags.def
@@ -691,6 +691,7 @@ X(Global, nlsat_bug, "nlsat bug")
 X(Global, nlsat_evaluator, "nlsat evaluator")
 X(Global, nlsat_evaluator_bug, "nlsat evaluator bug")
 X(Global, nlsat_explain, "nlsat explain")
+X(Global, levelwise, "levelwise")
 X(Global, nlsat_factor, "nlsat factor")
 X(Global, nlsat_fd, "nlsat fd")
 X(Global, nlsat_inf_set, "nlsat inf set")