diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 6c81c24cc..52984a4b7 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -113,10 +113,7 @@ namespace polysat {
         SASSERT(empty());
         for (auto lit : cl) {
             auto c = s.lit2cnstr(lit);
-            if (c.bvalue(s) != l_false) {
-                SASSERT(c.is_currently_false(s));
-                c->set_var_dependent();               
-            }
+            SASSERT(c.bvalue(s) == l_false);
             insert(~c);            
         }
         SASSERT(!empty());
@@ -252,7 +249,7 @@ namespace polysat {
             auto eq = s.eq(s.var(v), s.get_value(v));
             cm().ensure_bvar(eq.get());
             if (eq.bvalue(s) == l_undef) 
-                s.assign_eval(s.get_level(v), eq.blit());            
+                s.assign_eval(eq.blit());            
             lemma.push(~eq);
         }        
         s.decay_activity();
diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index b7035ef23..62996793a 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -88,8 +88,15 @@ namespace polysat {
             if (m_bvars.is_false(cl[i]))
                 continue;
             signed_constraint sc = s.lit2cnstr(cl[i]);
-            if (sc.is_currently_false(s)) 
-                continue;            
+            if (sc.is_currently_false(s)) {
+                if (m_bvars.is_true(cl[i])) {
+                    s.set_conflict(sc);
+                    return;
+                }
+                s.assign_eval(~cl[i]);
+                continue;
+            }
+            
             m_bvars.watch(cl[i]).push_back(&cl);
             std::swap(cl[!first], cl[i]);
             if (!first)
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 0d3266f24..53307ce23 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -596,10 +596,8 @@ namespace polysat {
             case l_false:
                 break;
             case l_undef:               
-                if (lit2cnstr(lit).is_currently_false(*this)) {
-                    unsigned level = m_level; // TODO
-                    assign_eval(level, lit);
-                }
+                if (lit2cnstr(lit).is_currently_false(*this)) 
+                    assign_eval(lit);                
                 else {
                     num_choices++;
                     choice = lit;
@@ -732,7 +730,10 @@ namespace polysat {
         m_search.push_boolean(lit);
     }
 
-    void solver::assign_eval(unsigned level, sat::literal lit) {
+    void solver::assign_eval(sat::literal lit) {
+        unsigned level = 0;
+        for (auto v : lit2cnstr(lit)->vars())
+            level = std::max(get_level(v), level);
         m_bvars.eval(lit, level);
         m_trail.push_back(trail_instr_t::assign_bool_i);
         m_search.push_boolean(lit);
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 35231273c..2a1a5f37a 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -149,7 +149,7 @@ namespace polysat {
 
         void assign_propagate(sat::literal lit, clause& reason);
         void assign_decision(sat::literal lit, clause* lemma);
-        void assign_eval(unsigned level, sat::literal lit);
+        void assign_eval(sat::literal lit);
         void activate_constraint(signed_constraint c);
         void deactivate_constraint(signed_constraint c);
         void decide_bool(clause& lemma);