diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 865e2a03e..fdaf1347d 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -96,6 +96,7 @@ namespace dd {
     pdd pdd_manager::mul(pdd const& a, pdd const& b) { return pdd(apply(a.root, b.root, pdd_mul_op), this); }
     pdd pdd_manager::reduce(pdd const& a, pdd const& b) { return pdd(apply(a.root, b.root, pdd_reduce_op), this); }
     pdd pdd_manager::mk_val(rational const& r) { return pdd(imk_val(r), this); }
+    pdd pdd_manager::mk_val(unsigned r) { return mk_val(rational(r)); }
     pdd pdd_manager::mul(rational const& r, pdd const& b) { pdd c(mk_val(r)); return pdd(apply(c.root, b.root, pdd_mul_op), this); }
     pdd pdd_manager::add(rational const& r, pdd const& b) { pdd c(mk_val(r)); return pdd(apply(c.root, b.root, pdd_add_op), this); }
     pdd pdd_manager::zero() { return pdd(zero_pdd, this); }
@@ -103,6 +104,7 @@ namespace dd {
     
     pdd pdd_manager::mk_or(pdd const& p, pdd const& q) { return p + q - (p*q); }
     pdd pdd_manager::mk_xor(pdd const& p, pdd const& q) { if (m_semantics == mod2_e) return p + q; return (p*q*2) - p - q; }
+    pdd pdd_manager::mk_xor(pdd const& p, unsigned x) { pdd q(mk_val(x)); if (m_semantics == mod2_e) return p + q; return (p*q*2) - p - q; }
     pdd pdd_manager::mk_not(pdd const& p) { return 1 - p; }
 
     pdd pdd_manager::subst_val(pdd const& p, vector<std::pair<unsigned, rational>> const& _s) {
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 26eaa0628..8da53d55d 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -253,6 +253,7 @@ namespace dd {
 
         pdd mk_var(unsigned i);
         pdd mk_val(rational const& r);
+        pdd mk_val(unsigned r);
         pdd zero(); 
         pdd one(); 
         pdd minus(pdd const& a);
@@ -263,6 +264,7 @@ namespace dd {
         pdd mul(rational const& c, pdd const& b);
         pdd mk_or(pdd const& p, pdd const& q);
         pdd mk_xor(pdd const& p, pdd const& q);
+        pdd mk_xor(pdd const& p, unsigned q);
         pdd mk_not(pdd const& p);
         pdd reduce(pdd const& a, pdd const& b);
         pdd subst_val(pdd const& a, vector<std::pair<unsigned, rational>> const& s);
@@ -325,6 +327,7 @@ namespace dd {
         pdd operator&(pdd const& other) const { return m.mul(*this, other); }
         pdd operator|(pdd const& other) const { return m.mk_or(*this, other); }
         pdd operator^(pdd const& other) const { return m.mk_xor(*this, other); }        
+        pdd operator^(unsigned other) const { return m.mk_xor(*this, other); }        
 
         pdd operator*(rational const& other) const { return m.mul(other, *this); }
         pdd operator+(rational const& other) const { return m.add(other, *this); }
@@ -360,6 +363,9 @@ namespace dd {
     inline pdd operator+(int x, pdd const& b) { return b + rational(x); }
     inline pdd operator+(pdd const& b, int x) { return b + rational(x); }
 
+    inline pdd operator^(unsigned x, pdd const& b) { return b + x; }
+    inline pdd operator^(bool x, pdd const& b) { return b + x; }
+
     inline pdd operator-(rational const& r, pdd const& b) { return b.rev_sub(r); }
     inline pdd operator-(int x, pdd const& b) { return rational(x) - b; }
     inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); }
diff --git a/src/sat/sat_anf_simplifier.cpp b/src/sat/sat_anf_simplifier.cpp
index ec56b6156..4ff8daeca 100644
--- a/src/sat/sat_anf_simplifier.cpp
+++ b/src/sat/sat_anf_simplifier.cpp
@@ -372,9 +372,7 @@ namespace sat {
 
     void anf_simplifier::add_bin(solver::bin_clause const& b, pdd_solver& ps) {
         auto& m = ps.get_manager();
-        auto v = lit2pdd(b.first);
-        auto w = lit2pdd(b.second);
-        dd::pdd p = (v | w) + 1;
+        dd::pdd p = (lit2pdd(b.first) | lit2pdd(b.second)) ^ true;
         ps.add(p);
         TRACE("anf_simplifier", tout << "bin: " << b.first << " " << b.second << " : " << p << "\n";);
     }
@@ -384,7 +382,7 @@ namespace sat {
         auto& m = ps.get_manager();
         dd::pdd p = m.zero();
         for (literal l : c) p |= lit2pdd(l);
-        p = p + 1;
+        p = p ^ true;
         ps.add(p);
         TRACE("anf_simplifier", tout << "clause: " << c << " : " << p << "\n";);
     }
@@ -408,7 +406,8 @@ namespace sat {
 
     void anf_simplifier::add_if(literal head, literal c, literal th, literal el, pdd_solver& ps) {
         auto& m = ps.get_manager();
-        dd::pdd p = lit2pdd(head) ^ (lit2pdd(c) & lit2pdd(th)) ^ (~lit2pdd(c) & lit2pdd(el));        
+        dd::pdd cond = lit2pdd(c);
+        dd::pdd p = lit2pdd(head) ^ (cond & lit2pdd(th)) ^ (~cond & lit2pdd(el));        
         ps.add(p);
         TRACE("anf_simplifier", tout << "ite: " << head << " == " << c << "?" << th << ":" << el << " poly : " << p << "\n";);
     }