diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index b5c688d37..6892ee80e 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -35,11 +35,11 @@ namespace nlsat {
     struct levelwise::impl {
         struct property {
             prop_enum prop;
-            polynomial_ref   p;
+            polynomial_ref   poly;
             unsigned         s_idx = -1; // index of the root function, if applicable; -1 means unspecified
             unsigned         level = -1;  // -1 means unspecified
-            property(prop_enum pr, polynomial_ref const & pp, int si, int lvl) : prop(pr), p(pp), s_idx(si), level(lvl) {}
-            property(prop_enum pr, polynomial_ref const & pp) : prop(pr), p(pp), s_idx(-1), level(-1) {}
+            property(prop_enum pr, polynomial_ref const & pp, int si, int lvl) : prop(pr), poly(pp), s_idx(si), level(lvl) {}
+            property(prop_enum pr, polynomial_ref const & pp) : prop(pr), poly(pp), s_idx(-1), level(-1) {}
         };
         solver& m_solver;
         polynomial_ref_vector const& m_P;
@@ -155,7 +155,7 @@ namespace nlsat {
                 if (level < m_n)
                     Q.push_back(property(prop_enum::sgn_inv_irreducible, polynomial_ref(p, m_pm), /*s_idx*/0u, /* level */ level));
                 else if (level == m_n) 
-                    Q.push_back(property(prop_enum::an_del, polynomial_ref(p, m_pm), /* s_idx*/ 0u, level));   
+                    Q.push_back(property(prop_enum::an_del, polynomial_ref(p, m_pm), /* s_idx */ -1, level));   
                 else {
                     SASSERT(level <= m_n);
                 }    
@@ -243,7 +243,7 @@ namespace nlsat {
         };
 
         bool dominates(const property& a, const property& b) const {
-            return a.p == b.p && dominates(a.prop, b.prop);
+            return a.poly == b.poly && dominates(a.prop, b.prop);
         }
         bool dominates(prop_enum a, prop_enum b) const {
             return m_prop_dom[static_cast<unsigned>(a)][static_cast<unsigned>(b)];
@@ -270,12 +270,12 @@ namespace nlsat {
         }
 
         std::ostream& display(std::ostream& out, const property & pr) {
-            out << "{prop:" << prop_name(pr.prop)
-                << ", level:" << pr.level
-                << ", s_idx:" << pr.s_idx;
-            if (pr.p) {
-                out << ", p:";
-                ::nlsat::display(out, m_solver, pr.p);
+            out << "{prop:" << prop_name(pr.prop);
+            if (pr.level != -1) out   << ", level:" << pr.level;
+            if (pr.s_idx != -1) out   << ", s_idx:" << pr.s_idx;
+            if (pr.poly) {
+                out << ", poly:";
+                ::nlsat::display(out, m_solver, pr.poly);
             }
             else {
                 out << ", p:null";
@@ -311,7 +311,7 @@ namespace nlsat {
             keys.reserve(cand.size());
             for (size_t i = 0; i < cand.size(); ++i) {
                 if (!dominated[i]) {
-                    keys.push_back(Key{ polynomial::manager::id(cand[i].p.get()), static_cast<unsigned>(cand[i].prop), i });
+                    keys.push_back(Key{ polynomial::manager::id(cand[i].poly.get()), static_cast<unsigned>(cand[i].prop), i });
                 }
             }
             std::sort(keys.begin(), keys.end(), [](Key const& a, Key const& b){
@@ -483,8 +483,8 @@ namespace nlsat {
         void build_representation(unsigned i, result_struct& ret) {
             std::vector<const poly*> p_non_null;
             for (const auto & pr: m_Q) {
-                if (pr.prop == prop_enum::sgn_inv_irreducible && max_var(pr.p) == i && poly_is_not_nullified_at_sample_at_level(pr.p.get(), i))
-                    p_non_null.push_back(pr.p.get());
+                if (pr.prop == prop_enum::sgn_inv_irreducible && max_var(pr.poly) == i && poly_is_not_nullified_at_sample_at_level(pr.poly.get(), i))
+                    p_non_null.push_back(pr.poly.get());
             }
             std::vector<std::unique_ptr<bucket_t>> buckets;
             std::vector<root_item_t> roots;
@@ -516,7 +516,7 @@ namespace nlsat {
         }
 
         void apply_pre(const property& p) {
-            TRACE(levelwise, display(tout << "p:", p) << std::endl;);
+            TRACE(levelwise, display(tout << "property p:", p) << std::endl;);
             NOT_IMPLEMENTED_YET();
         }
         // return an empty vector on failure, otherwis returns the cell representations with intervals