diff --git a/src/sat/smt/polysat/polysat_core.cpp b/src/sat/smt/polysat/polysat_core.cpp
index 09bfbd244..ff35f20ee 100644
--- a/src/sat/smt/polysat/polysat_core.cpp
+++ b/src/sat/smt/polysat/polysat_core.cpp
@@ -67,13 +67,13 @@ namespace polysat {
     public:
         mk_add_watch(core& c) : c(c) {}
         void undo() override {
-            auto& [sc, lit] = c.m_constraint_trail.back();
+            auto& [sc, lit, val] = c.m_constraint_index.back();
             auto& vars = sc.vars();
             if (vars.size() > 0)
                 c.m_watch[vars[0]].pop_back();
             if (vars.size() > 1)
                 c.m_watch[vars[1]].pop_back();
-            c.m_constraint_trail.pop_back();
+            c.m_constraint_index.pop_back();
         }
     };
 
@@ -121,8 +121,8 @@ namespace polysat {
     }
 
     unsigned core::register_constraint(signed_constraint& sc, dependency d) {
-        unsigned idx = m_constraint_trail.size();
-        m_constraint_trail.push_back({ sc, d });
+        unsigned idx = m_constraint_index.size();
+        m_constraint_index.push_back({ sc, d, l_undef });
         auto& vars = sc.vars();
         unsigned i = 0, j = 0, sz = vars.size();
         for (; i < sz && j < 2; ++i)
@@ -177,7 +177,7 @@ namespace polysat {
     }
 
     signed_constraint core::get_constraint(unsigned idx, bool sign) {
-        auto sc = m_constraint_trail[idx].sc;
+        auto sc = m_constraint_index[idx].sc;
         if (sign)
             sc = ~sc;
         return sc;
@@ -212,7 +212,7 @@ namespace polysat {
         // for entries where there is only one free variable left add to viable set 
         unsigned j = 0;
         for (auto idx : m_watch[v]) {
-            auto [sc, as] = m_constraint_trail[idx];
+            auto [sc, as, value] = m_constraint_index[idx];
             auto& vars = sc.vars();
             if (vars[0] != v)
                 std::swap(vars[0], vars[1]);
@@ -263,7 +263,7 @@ namespace polysat {
             for (auto idx1 : m_watch[m_var]) {
                 if (idx == idx1)
                     continue;
-                auto [sc, d] = m_constraint_trail[idx1];
+                auto [sc, d, value] = m_constraint_index[idx1];
                 switch (eval(sc)) {
                 case l_false:
                     s.propagate(d, true, explain_eval(sc));
@@ -298,8 +298,18 @@ namespace polysat {
     }
 
     void core::assign_eh(unsigned index, bool sign, dependency const& dep) { 
+        struct unassign : public trail {
+            core& c;
+            unsigned m_index;
+            unassign(core& c, unsigned index): c(c), m_index(index) {}
+            void undo() override {
+                c.m_constraint_index[m_index].value = l_undef;
+                c.m_prop_queue.pop_back();
+            }
+        };
         m_prop_queue.push_back({ index, sign, dep });
-        s.trail().push(push_back_vector(m_prop_queue));
+        m_constraint_index[index].value = to_lbool(!sign);
+        s.trail().push(unassign(*this, index));
     }
 
     dependency_vector core::explain_eval(signed_constraint const& sc) { 
diff --git a/src/sat/smt/polysat/polysat_core.h b/src/sat/smt/polysat/polysat_core.h
index b5b7dd380..b4f35e776 100644
--- a/src/sat/smt/polysat/polysat_core.h
+++ b/src/sat/smt/polysat/polysat_core.h
@@ -42,8 +42,9 @@ namespace polysat {
         friend class assignment;
 
         struct constraint_info {
-            signed_constraint sc;
-            dependency d;
+            signed_constraint sc;        // signed constraint representation
+            dependency d;                // justification for constraint
+            lbool      value;            // value assigned by solver
         };
         solver_interface& s;
         viable m_viable;
@@ -51,7 +52,7 @@ namespace polysat {
         assignment m_assignment;
         unsigned m_qhead = 0, m_vqhead = 0;
         svector<prop_item> m_prop_queue;
-        svector<constraint_info> m_constraint_trail;  // index of constraints
+        svector<constraint_info> m_constraint_index;  // index of constraints
         mutable scoped_ptr_vector<dd::pdd_manager> m_pdd;
         dependency_vector m_unsat_core;
 
diff --git a/src/sat/smt/polysat/polysat_types.h b/src/sat/smt/polysat/polysat_types.h
index b9b440481..92896a7f7 100644
--- a/src/sat/smt/polysat/polysat_types.h
+++ b/src/sat/smt/polysat/polysat_types.h
@@ -89,6 +89,10 @@ namespace polysat {
 
     class signed_constraint;
 
+    //
+    // The interface that PolySAT uses to the SAT/SMT solver.
+    //
+
     class solver_interface {
     public:
         virtual void add_eq_literal(pvar v, rational const& val) = 0;
diff --git a/src/sat/smt/polysat/polysat_viable.cpp b/src/sat/smt/polysat/polysat_viable.cpp
index a8a9fd6af..8d9009af0 100644
--- a/src/sat/smt/polysat/polysat_viable.cpp
+++ b/src/sat/smt/polysat/polysat_viable.cpp
@@ -636,7 +636,7 @@ namespace polysat {
 
         if (c.is_assigned(v))
             return;
-        auto [sc, d] = c.m_constraint_trail[idx];
+        auto [sc, d, value] = c.m_constraint_index[idx];
         // fixme: constraint must be assigned a value l_true or l_false at this point.
         // adjust sc to the truth value of the constraint when passed to forbidden intervals.