diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp
index ada63336d..864da9e96 100644
--- a/src/sat/smt/polysat/core.cpp
+++ b/src/sat/smt/polysat/core.cpp
@@ -190,7 +190,8 @@ namespace polysat {
                 case l_true:
                     propagate_assignment(m_var, m_value, d);
                     break;
-                case l_false:                    
+                case l_false:   
+                    // add m_var != m_value to m_viable but need a constraint index for that.
                     m_value = mod(m_value + 1, rational::power_of_two(size(m_var)));
                     goto try_again;
                 default:
@@ -299,7 +300,7 @@ namespace polysat {
                 return;
             v = w;
         }
-        if (v != null_var && !m_viable.add_unitary(v, idx.id))
+        if (v != null_var && !m_viable.add_unitary(v, idx))
             s.set_conflict(m_viable.explain(), "viable-conflict");
     }
 
@@ -352,7 +353,7 @@ namespace polysat {
             if (!is_assigned(v0) || is_assigned(v1))
                 continue;
             // detect unitary, add to viable, detect conflict?
-            if (value != l_undef && !m_viable.add_unitary(v1, idx))
+            if (value != l_undef && !m_viable.add_unitary(v1, {idx}))
                 s.set_conflict(m_viable.explain(), "viable-conflict");
         }
         SASSERT(m_watch[v].size() == sz && "size of watch list was not changed");
diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h
index 1baee32eb..f9910deab 100644
--- a/src/sat/smt/polysat/types.h
+++ b/src/sat/smt/polysat/types.h
@@ -23,7 +23,8 @@ namespace polysat {
     using pvar = unsigned;
     using theory_var = unsigned;
     struct constraint_id {
-        unsigned id; bool is_null() const { return id == UINT_MAX; }
+        unsigned id = UINT_MAX; 
+        bool is_null() const { return id == UINT_MAX; }
         static constraint_id null() { return constraint_id{ UINT_MAX }; }
     };
 
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index 370f2236d..dc7a382a9 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -68,7 +68,7 @@ namespace polysat {
         }
     };
 
-    viable::entry* viable::alloc_entry(pvar var, unsigned constraint_index) {
+    viable::entry* viable::alloc_entry(pvar var, constraint_id constraint_index) {
         entry* e = nullptr;
         if (m_alloc.empty())
             e = alloc(entry);
@@ -532,12 +532,12 @@ namespace polysat {
         uint_set seen;
         for (auto e : m_explain) {
             auto index = e->constraint_index;
-            if (seen.contains(index))
+            if (seen.contains(index.id))
                 continue;
             if (m_var != e->var)
                 result.push_back(offset_claim(m_var, {e->var, 0}));
-            seen.insert(index);
-            auto const& [sc, d, value] = c.m_constraint_index[index];
+            seen.insert(index.id);
+            auto const& [sc, d, value] = c.m_constraint_index[index.id];
             result.push_back(d);
             result.append(c.explain_eval(sc));
         }
@@ -548,11 +548,11 @@ namespace polysat {
     /*
     * Register constraint at index 'idx' as unitary in v.
     */
-    bool viable::add_unitary(pvar v, unsigned idx) {
+    bool viable::add_unitary(pvar v, constraint_id idx) {
 
         if (c.is_assigned(v))
             return true;
-        auto [sc, d, value] = c.m_constraint_index[idx];
+        auto [sc, d, value] = c.m_constraint_index[idx.id];
         SASSERT(value != l_undef);
         if (value == l_false)
             sc = ~sc;
diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h
index 5ac17e31c..7f3788e15 100644
--- a/src/sat/smt/polysat/viable.h
+++ b/src/sat/smt/polysat/viable.h
@@ -53,7 +53,7 @@ namespace polysat {
             bool active = true;
             bool valid_for_lemma = true;
             pvar var = null_var;
-            unsigned constraint_index = UINT_MAX;
+            constraint_id constraint_index;
 
             void reset() {
                 // dll_base<entry>::init(this);  // we never did this in alloc_entry either
@@ -62,7 +62,7 @@ namespace polysat {
                 active = true;
                 valid_for_lemma = true;
                 var = null_var;
-                constraint_index = UINT_MAX;
+                constraint_index = constraint_id::null();
             }
         };
 
@@ -97,7 +97,7 @@ namespace polysat {
         bool well_formed(entry* e);
         bool well_formed(layers const& ls);
 
-        entry* alloc_entry(pvar v, unsigned constraint_index);
+        entry* alloc_entry(pvar v, constraint_id constraint_index);
 
         std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const;
         std::ostream& display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter = "") const;
@@ -152,7 +152,7 @@ namespace polysat {
         /*
         * Register constraint at index 'idx' as unitary in v.
         */
-        bool add_unitary(pvar v, unsigned idx);
+        bool add_unitary(pvar v, constraint_id);
 
         /*
         * Ensure data-structures tracking variable v.