diff --git a/src/math/polynomial/polynomial_cache.cpp b/src/math/polynomial/polynomial_cache.cpp
index d5953243c..7889ce674 100644
--- a/src/math/polynomial/polynomial_cache.cpp
+++ b/src/math/polynomial/polynomial_cache.cpp
@@ -128,7 +128,7 @@ namespace polynomial {
             m_factor_cache.reset();
         }
 
-        unsigned pid(polynomial * p) const { return m.id(p); }
+        unsigned pid(const polynomial * p) const { return m.id(p); }
         
         polynomial * mk_unique(polynomial * p) {
             if (m_in_cache.get(pid(p), false))
@@ -141,6 +141,10 @@ namespace polynomial {
             return p_prime;
         }
 
+        bool contains(const polynomial * p) const {
+            return m_in_cache.get(pid(p), false);
+        }
+
         void psc_chain(polynomial * p, polynomial * q, var x, polynomial_ref_vector & S) {
             p = mk_unique(p);
             q = mk_unique(q);
@@ -213,6 +217,10 @@ namespace polynomial {
         return m_imp->mk_unique(p);
     }
 
+    bool cache::contains(const polynomial * p) const {
+        return m_imp->contains(p);
+    }
+
     void cache::psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S) {
         m_imp->psc_chain(const_cast<polynomial*>(p), const_cast<polynomial*>(q), x, S);
     }
diff --git a/src/math/polynomial/polynomial_cache.h b/src/math/polynomial/polynomial_cache.h
index fbd70e500..e3241aa41 100644
--- a/src/math/polynomial/polynomial_cache.h
+++ b/src/math/polynomial/polynomial_cache.h
@@ -34,6 +34,7 @@ namespace polynomial {
         manager & m() const;
         manager & pm() const { return m(); }
         polynomial * mk_unique(polynomial * p);
+        bool contains(const polynomial * p) const;
         void psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S);
         void factor(polynomial const * p, polynomial_ref_vector & distinct_factors);
         void reset();
diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index 663aa7893..3e084c63b 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -227,7 +227,7 @@ namespace nlsat {
         void collect_top_level_properties(todo_set& ps_of_n_level) {
             for (unsigned i = 0; i < m_P.size(); ++i) {
                 polynomial_ref pi(m_P[i], m_pm);
-                for_each_distinct_factor(pi, [&](const polynomial_ref& f) {
+                for_each_distinct_factor(pi, [&](polynomial_ref f) {
                     unsigned level = max_var(f);
                     normalize(f);
                     if (level < m_n)
@@ -300,7 +300,7 @@ namespace nlsat {
                     fail();
                     return false;
                 }
-                for_each_distinct_factor(r, [&](const polynomial::polynomial_ref &f) {
+                for_each_distinct_factor(r, [&](polynomial::polynomial_ref f) {
                     normalize(f);
                     m_Q[max_var(f)].push(property(prop_enum::ord_inv, f, m_pm));
                 });
@@ -501,9 +501,10 @@ namespace nlsat {
              TRACE(lws, tout << "exit\n";);
          }
 
-         void normalize(polynomial_ref const & p) {
-             SASSERT(! (is_zero(p) || is_const(p)));
-             m_todo_set.insert(p);
+         void normalize(polynomial_ref & p) {
+             SASSERT(!(is_zero(p) || is_const(p)));
+             poly* np = m_todo_set.insert(p);
+             p = np;
         }
 
 
@@ -559,9 +560,11 @@ namespace nlsat {
                 });
             }
          }
-
+        
+        
         //  handle sgn_inv(leading_coefficient_{x_{i+1}}(p)) for an_del pre-processing
         void add_sgn_inv_leading_coeff_for(const property& p) {
+            TRACE(lws, tout << "p:"; display(tout, p) << "\n";);
             poly * pp = p.m_poly.get();
             unsigned lvl = max_var(p.m_poly);
             unsigned deg = m_pm.degree(pp, lvl);
@@ -572,11 +575,12 @@ namespace nlsat {
             for (int d = static_cast<int>(deg); d >= 0; --d) {
                 coeff = m_pm.coeff(pp, lvl, d);
                 if (!is_const(coeff)) {
-                    for_each_distinct_factor(coeff, [&](const polynomial::polynomial_ref & f) {
+                    for_each_distinct_factor(coeff, [&](polynomial::polynomial_ref f) {
                         normalize(f);
                         mk_prop(prop_enum::sgn_inv, f, max_var(f));
                     });
                 }
+                TRACE(lws, tout << "coeff:" << coeff << "\n";);
 
                 if (sign(coeff, sample(), m_am))
                     return;
@@ -789,11 +793,11 @@ or
             add_to_Q_if_new(property(pe, m_pm), level.val);
         }
 
-        void mk_prop(prop_enum pe, const polynomial_ref& poly) {
+        void mk_prop(prop_enum pe, polynomial_ref poly) {
             normalize(poly);
             add_to_Q_if_new(property(pe, poly), max_var(poly));
         }
-        void mk_prop(prop_enum pe, const polynomial_ref& poly, unsigned level) {
+        void mk_prop(prop_enum pe, polynomial_ref poly, unsigned level) {
             SASSERT(is_set(level));
             normalize(poly);
             add_to_Q_if_new(property(pe, poly), level);
@@ -840,7 +844,8 @@ or
                 if (I.l == p.m_poly.get()) {
                     // nothing is added
                 } else {
-                    polynomial_ref res = resultant(polynomial_ref(I.l, m_pm), p.m_poly, m_level);
+                    polynomial_ref res = resultant(I.l, p.m_poly, m_level);
+                    SASSERT(m_todo_set.contains(I.l) && m_todo_set.contains(p.m_poly));
                     TRACE(lws,
                           tout << "m_level:" << m_level<< "\nresultant of (" << I.l << "," << p.m_poly << "):"; 
                           tout << "\nresultant:"; ::nlsat::display(tout, m_solver, res) << "\n");
@@ -909,6 +914,7 @@ or
         void apply_pre(const property& p) {
             TRACE(lws, tout << "apply_pre BEGIN m_Q:"; display(tout) << std::endl; 
                   display(tout << "pre p:", p) << std::endl;);
+            SASSERT(!p.m_poly || m_todo_set.contains(p.m_poly));
             switch (p.m_prop_tag) {
             case prop_enum::an_del:
                 apply_pre_an_del(p);
diff --git a/src/nlsat/nlsat_common.cpp b/src/nlsat/nlsat_common.cpp
index 602784943..405408d87 100644
--- a/src/nlsat/nlsat_common.cpp
+++ b/src/nlsat/nlsat_common.cpp
@@ -30,7 +30,7 @@ namespace nlsat {
         m_set.reset();
     }
 
-    void todo_set::insert(poly* p) {
+    poly* todo_set::insert(poly* p) {
         pmanager& pm = m_set.m();
         polynomial_ref pinned(pm); // keep canonicalized polynomial alive until it is stored
         if (m_canonicalize) {
@@ -47,12 +47,17 @@ namespace nlsat {
         }
         p = m_cache.mk_unique(p);
         unsigned pid = pm.id(p);
-        if (m_in_set.get(pid, false))
-            return;
-        m_in_set.setx(pid, true, false);
-        m_set.push_back(p);
+        if (!m_in_set.get(pid, false)) {
+            m_in_set.setx(pid, true, false);
+            m_set.push_back(p);
+        }
+        return p;
     }
 
+    bool todo_set::contains(poly* p) const {
+        return m_cache.contains(p);
+    }
+    
     bool todo_set::empty() const { return m_set.empty(); }
 
     // Return max variable in todo_set
diff --git a/src/nlsat/nlsat_common.h b/src/nlsat/nlsat_common.h
index 5b50e2fc3..c80204fbc 100644
--- a/src/nlsat/nlsat_common.h
+++ b/src/nlsat/nlsat_common.h
@@ -32,7 +32,9 @@ namespace nlsat {
         todo_set(polynomial::cache& u, bool canonicalize);
 
         void reset();
-        void insert(poly* p);
+        // Insert polynomial (canonicalizing if requested) and return the cached representative.
+        poly* insert(poly* p);
+        bool contains(poly *) const;
         bool empty() const;
         // Return max variable in todo_set
         var max_var() const;