diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 06735cec4..6c81c24cc 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -111,8 +111,14 @@ namespace polysat {
             return;
         LOG("Conflict: " << cl);
         SASSERT(empty());
-        for (auto lit : cl)          
-            insert(~s.lit2cnstr(lit));        
+        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();               
+            }
+            insert(~c);            
+        }
         SASSERT(!empty());
     }
 
diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index f62a76afa..31f20cc71 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -34,6 +34,17 @@ namespace polysat {
         for (auto v : r.free_vars())
             if (!m_vars.contains(v))
                 m_vars.push_back(v);
+
+        switch (c) {
+        case code::and_op:
+        case code::or_op:
+        case code::xor_op:
+            if (p.index() > q.index())
+                std::swap(m_p, m_q);
+            break;
+        default:
+            break;
+        }
     }
 
     lbool op_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
diff --git a/src/math/polysat/trail.h b/src/math/polysat/trail.h
index 8ee6e81c1..2b3657157 100644
--- a/src/math/polysat/trail.h
+++ b/src/math/polysat/trail.h
@@ -16,7 +16,7 @@ Author:
 
 namespace polysat {
 
-    enum trail_instr_t { 
+    enum class trail_instr_t { 
         qhead_i,
         add_var_i,
         inc_level_i,
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 4a432401a..617513a3e 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -980,6 +980,15 @@ namespace polysat {
     }
 
     static void test_band(unsigned bw = 32) {
+        {
+            scoped_solver s(__func__);
+            auto p = s.var(s.add_var(bw));
+            auto q = s.var(s.add_var(bw));
+            s.add_diseq(p - s.band(p, q));
+            s.add_diseq(p - q);
+            s.check();
+            s.expect_sat();
+        }
         {
             scoped_solver s(__func__);
             auto p = s.var(s.add_var(bw));
@@ -1004,6 +1013,16 @@ namespace polysat {
             s.check();
             s.expect_sat();
         }
+        {
+            scoped_solver s(__func__);
+            auto p = s.var(s.add_var(bw));
+            auto q = s.var(s.add_var(bw));
+            s.add_ule(p, s.band(p, q));
+            s.add_diseq(p - s.band(p, q));
+            s.check();
+            s.expect_unsat();
+        }
+ 
 
     }