diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 848453aca..d0acd82c1 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -23,13 +23,13 @@ Revision History:
 
 namespace dd {
 
-    pdd_manager::pdd_manager(unsigned num_vars) {
+    pdd_manager::pdd_manager(unsigned num_vars, semantics s) {
         m_spare_entry = nullptr;
         m_max_num_nodes = 1 << 24; // up to 16M nodes
         m_mark_level = 0;
         m_disable_gc = false;
         m_is_new_node = false;
-        m_mod2_semantics = false;
+        m_semantics = s;
 
         // add dummy nodes for operations, and 0, 1 pdds.
         for (unsigned i = 0; i < pdd_no_op; ++i) {
@@ -61,7 +61,7 @@ namespace dd {
     }
 
     pdd pdd_manager::add(pdd const& a, pdd const& b) { return pdd(apply(a.root, b.root, pdd_add_op), this); }
-    pdd pdd_manager::sub(pdd const& a, pdd const& b) { pdd m(minus(b)); return pdd(apply(a.root, m.root, pdd_add_op), this); }
+    pdd pdd_manager::sub(pdd const& a, pdd const& b) { return pdd(apply(a.root, b.root, pdd_sub_op), this); }
     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); }
@@ -71,6 +71,8 @@ namespace dd {
     pdd pdd_manager::one() { return pdd(one_pdd, this); }
     
     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) { return (p*q*2) - p - q; }
+    pdd pdd_manager::mk_not(pdd const& p) { return 1 - p; }
 
     pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
         bool first = true;
@@ -108,6 +110,11 @@ namespace dd {
 
     pdd_manager::PDD pdd_manager::apply_rec(PDD p, PDD q, pdd_op op) {
         switch (op) {
+        case pdd_sub_op:
+            if (is_zero(q)) return p;
+            if (is_val(p) && is_val(q)) return imk_val(val(p) - val(q));
+            if (m_semantics != mod2_e) break;
+            op = pdd_add_op;
         case pdd_add_op:
             if (is_zero(p)) return q;
             if (is_zero(q)) return p;
@@ -163,6 +170,35 @@ namespace dd {
                 npop = 1;
             }
             break;
+        case pdd_sub_op:
+            if (is_val(p)) {
+                push(apply_rec(p, lo(q), op));
+                r = make_node(level_q, read(1), hi(q));
+                npop = 1;                
+            }
+            else if (is_val(q)) {
+                push(apply_rec(lo(p), q, op));
+                r = make_node(level_p, read(1), hi(p));
+                npop = 1;
+            }
+            else if (level_p == level_q) {
+                push(apply_rec(lo(p), lo(q), op));
+                push(apply_rec(hi(p), hi(q), op));
+                r = make_node(level_p, read(2), read(1));                           
+            }
+            else if (level_p > level_q) {
+                // x*hi(p) + (lo(p) - q)
+                push(apply_rec(lo(p), q, op));
+                r = make_node(level_p, read(1), hi(p));
+                npop = 1;
+            }
+            else {
+                // x*hi(q) + (p - lo(q))
+                push(apply_rec(p, lo(q), op));
+                r = make_node(level_q, read(1), hi(q));
+                npop = 1;                
+            }
+            break;
         case pdd_mul_op:
             SASSERT(!is_val(p));
             if (is_val(q)) {
@@ -171,17 +207,18 @@ namespace dd {
                 r = make_node(level_p, read(2), read(1));
             }
             else if (level_p == level_q) {
-                if (m_mod2_semantics) {
+                if (m_semantics != free_e) {
                     //
-                    // (xa+b)*(xc+d) mod2 == x(ac+bc+ad) + bd
-                    //                    == x((a+b)(c+d)+bd) + bd
+                    // (xa+b)*(xc+d)  == x(ac+bc+ad) + bd
+                    //                == x((a+b)(c+d)-bd) + bd
+                    // because x*x = x
                     //
                     push(apply_rec(lo(p), lo(q), pdd_mul_op));
                     unsigned bd = read(1);
                     push(apply_rec(hi(p), lo(p), pdd_add_op));
                     push(apply_rec(hi(q), lo(q), pdd_add_op));
                     push(apply_rec(read(1), read(2), pdd_mul_op));
-                    push(apply_rec(read(1), bd, pdd_add_op));
+                    push(apply_rec(read(1), bd, pdd_sub_op));
                     r = make_node(level_p, bd, read(1));
                     npop = 5;
                 }
@@ -243,7 +280,7 @@ namespace dd {
     }
 
     pdd pdd_manager::minus(pdd const& a) {
-        if (m_mod2_semantics) {
+        if (m_semantics == mod2_e) {
             return a;
         }
         bool first = true;
@@ -264,7 +301,7 @@ namespace dd {
     }
 
     pdd_manager::PDD pdd_manager::minus_rec(PDD a) {
-        SASSERT(!m_mod2_semantics);
+        SASSERT(m_semantics != mod2_e);
         if (is_zero(a)) return zero_pdd;
         if (is_val(a)) return imk_val(-val(a));
         op_entry* e1 = pop_entry(a, a, pdd_minus_op);
@@ -358,7 +395,7 @@ namespace dd {
                 while (!is_val(x)) p.push_back(var(x)), x = hi(x);
                 pc = val(x);
                 qc = val(y);
-                if (!m_mod2_semantics && pc.is_int() && qc.is_int()) {
+                if (m_semantics != mod2_e && pc.is_int() && qc.is_int()) {
                     rational g = gcd(pc, qc);
                     pc /= g;
                     qc /= g;
@@ -461,6 +498,17 @@ namespace dd {
         return is_binary(p.root); 
     }
 
+    /**
+       Determine if p is a monomial.
+    */
+    bool pdd_manager::is_monomial(PDD p) {
+        while (true) {
+            if (is_val(p)) return true;
+            if (!is_zero(lo(p))) return false;
+            p = hi(p);
+        }
+    }
+
     /*
       \brief determine if v occurs as a leaf variable.
      */
@@ -522,7 +570,7 @@ namespace dd {
     pdd_manager::PDD pdd_manager::imk_val(rational const& r) {
         if (r.is_zero()) return zero_pdd;
         if (r.is_one()) return one_pdd;
-        if (m_mod2_semantics) return imk_val(mod(r, rational(2)));
+        if (m_semantics == mod2_e) return imk_val(mod(r, rational(2)));
         const_info info;
         if (!m_mpq_table.find(r, info)) {
             init_value(info, r);
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 0c0139611..506fd0238 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -41,6 +41,9 @@ namespace dd {
     class pdd;
 
     class pdd_manager {
+    public:
+        enum semantics { free_e, mod2_e, zero_one_vars_e };
+    private:
         friend pdd;
 
         typedef unsigned PDD;
@@ -52,10 +55,11 @@ namespace dd {
 
         enum pdd_op {
             pdd_add_op = 2,
-            pdd_minus_op = 3,
-            pdd_mul_op = 4,
-            pdd_reduce_op = 5,
-            pdd_no_op = 6
+            pdd_sub_op = 3,
+            pdd_minus_op = 4,
+            pdd_mul_op = 5,
+            pdd_reduce_op = 6,
+            pdd_no_op = 7
         };
 
         struct node {
@@ -151,7 +155,7 @@ namespace dd {
         bool                       m_disable_gc;
         bool                       m_is_new_node;
         unsigned                   m_max_num_nodes;
-        bool                       m_mod2_semantics;
+        semantics                  m_semantics;
         unsigned_vector            m_free_vars;
         unsigned_vector            m_free_values;
         rational                   m_freeze_value;
@@ -230,10 +234,9 @@ namespace dd {
 
         struct mem_out {};
 
-        pdd_manager(unsigned nodes);
+        pdd_manager(unsigned nodes, semantics s = free_e);
         ~pdd_manager();
 
-        void set_mod2_semantics() { m_mod2_semantics = true; }
         void set_max_num_nodes(unsigned n) { m_max_num_nodes = n; }
         void set_level2var(unsigned_vector const& level2var);  
         unsigned_vector const& get_level2var() const { return m_level2var; }
@@ -249,6 +252,8 @@ namespace dd {
         pdd mul(pdd const& a, pdd const& b);
         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_not(pdd const& p);
         pdd reduce(pdd const& a, pdd const& b);
 
         bool is_linear(PDD p);
@@ -257,6 +262,8 @@ namespace dd {
         bool is_binary(PDD p);
         bool is_binary(pdd const& p);
 
+        bool is_monomial(PDD p);
+
         // create an spoly r if leading monomials of a and b overlap
         bool try_spoly(pdd const& a, pdd const& b, pdd& r);
 
@@ -293,22 +300,28 @@ namespace dd {
         bool is_zero() const { return m.is_zero(root); }
         bool is_linear() const { return m.is_linear(root); }
         bool is_binary() const { return m.is_binary(root); }
+        bool is_monomial() const { return m.is_monomial(root); }
         bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
 
-        pdd minus() const { return m.minus(*this); }
+        pdd operator-() const { return m.minus(*this); }
         pdd operator+(pdd const& other) const { return m.add(*this, other); }
         pdd operator-(pdd const& other) const { return m.sub(*this, other); }
         pdd operator*(pdd const& other) const { return m.mul(*this, other); }
+        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*(rational const& other) const { return m.mul(other, *this); }
         pdd operator+(rational const& other) const { return m.add(other, *this); }
-        pdd operator|(pdd const& other) const { return m.mk_or(*this, other); }
+        pdd operator~() const { return m.mk_not(*this); }
+        pdd rev_sub(rational const& r) const { return m.sub(m.mk_val(r), *this); }
         pdd reduce(pdd const& other) const { return m.reduce(*this, other); }
         bool different_leading_term(pdd const& other) const { return m.different_leading_term(*this, other); }
 
         std::ostream& display(std::ostream& out) const { return m.display(out, *this); }
         bool operator==(pdd const& other) const { return root == other.root; }
         bool operator!=(pdd const& other) const { return root != other.root; }
-        bool operator<(pdd const& b) const { return m.lt(*this, b); }
+        bool operator<(pdd const& other) const { return m.lt(*this, other); }
 
         unsigned dag_size() const { return m.dag_size(*this); }
         double tree_size() const { return m.tree_size(*this); }
@@ -323,16 +336,17 @@ 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-(rational const& r, pdd const& b) { return r + b.minus(); }
+    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)); }
 
+    inline pdd& operator&=(pdd & p, pdd const& q) { p = p & q; return p; }
+    inline pdd& operator^=(pdd & p, pdd const& q) { p = p ^ q; return p; }
     inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; }
     inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; }
     inline pdd& operator-=(pdd & p, pdd const& q) { p = p - q; return p; }
     inline pdd& operator+=(pdd & p, pdd const& q) { p = p + q; return p; }
 
-
     std::ostream& operator<<(std::ostream& out, pdd const& b);
 
 }
diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp
index c05be15b4..3a102c044 100644
--- a/src/math/grobner/pdd_grobner.cpp
+++ b/src/math/grobner/pdd_grobner.cpp
@@ -186,13 +186,14 @@ namespace dd {
 
     void grobner::simplify() {
         try {
-            while (simplify_linear_step(true) || 
-                   simplify_elim_pure_step() ||
-                   simplify_linear_step(false) || 
-                   simplify_cc_step() || 
-                   simplify_leaf_step() ||
-                   /*simplify_elim_dual_step() ||*/
-                false) {
+            while (!done() &&
+                   (simplify_linear_step(true) || 
+                    simplify_elim_pure_step() ||
+                    simplify_cc_step() || 
+                    simplify_linear_step(false) || 
+                    simplify_leaf_step() ||
+                    /*simplify_elim_dual_step() ||*/
+                    false)) {
                 DEBUG_CODE(invariant(););
                 TRACE("grobner", display(tout););
             }
@@ -209,6 +210,7 @@ namespace dd {
     };
 
     bool grobner::simplify_linear_step(bool binary) {
+        TRACE("grobner", tout << "binary " << binary << "\n";);
         equation_vector linear;
         for (equation* e : m_to_simplify) {
             pdd p = e->poly();
@@ -243,12 +245,14 @@ namespace dd {
                     continue;
                 }
                 simplify_using(*dst, *src, changed_leading_term);
-                if (check_conflict(*dst)) {
-                    return false;
-                }
                 if (is_trivial(*dst)) {
                     trivial.push_back(dst);
                 }
+                else if (is_conflict(dst)) {
+                    pop_equation(dst);
+                    set_conflict(dst);
+                    return true;
+                }
                 else if (changed_leading_term) {
                     pop_equation(dst);
                     push_equation(to_simplify, dst);
@@ -257,7 +261,7 @@ namespace dd {
             if (all_reduced) {
                 linear[j++] = src;              
             }
-        } 
+        }
         linear.shrink(j);      
         for (equation* src : linear) {
             pop_equation(src);
@@ -277,6 +281,7 @@ namespace dd {
        since px = ry
      */
     bool grobner::simplify_cc_step() {
+        TRACE("grobner", tout << "cc\n";);
         u_map<equation*> los;
         bool reduced = false;
         unsigned j = 0;
@@ -309,6 +314,7 @@ namespace dd {
        \brief remove ax+b from p if x occurs as a leaf in p and a is a constant.
     */
     bool grobner::simplify_leaf_step() {
+        TRACE("grobner", tout << "leaf\n";);
         use_list_t use_list = get_use_list();
         bool reduced = false;
         equation_vector leaves;
@@ -329,8 +335,14 @@ namespace dd {
                 remove_from_use(e2, use_list);
                 simplify_using(*e2, *e, changed_leading_term);
                 add_to_use(e2, use_list);
-                if (check_conflict(*e2)) {
-                    return false;
+                if (is_trivial(*e2)) {
+                    pop_equation(e2);
+                    retire(e2);
+                }
+                else if (e2->poly().is_val()) {
+                    pop_equation(e2);
+                    set_conflict(*e2);
+                    return true;
                 }
                 else if (changed_leading_term) {
                     pop_equation(e2);
@@ -346,6 +358,7 @@ namespace dd {
        \brief treat equations as processed if top variable occurs only once.
     */
     bool grobner::simplify_elim_pure_step() {
+        TRACE("grobner", tout << "pure\n";);
         use_list_t use_list = get_use_list();        
         unsigned j = 0;
         for (equation* e : m_to_simplify) {
@@ -387,8 +400,9 @@ namespace dd {
 
                     remove_from_use(e2, use_list);
                     simplify_using(*e2, *e, changed_leading_term);
-                    if (check_conflict(*e2)) { 
-                        break;
+                    if (is_conflict(e2)) {
+                        pop_equation(e2);
+                        set_conflict(e2);
                     }
                     // when e2 is trivial, leading term is changed
                     SASSERT(!is_trivial(*e2) || changed_leading_term);
@@ -470,7 +484,7 @@ namespace dd {
         do {
             simplified = false;
             for (equation* p : eqs) {
-                if (simplify_source_target(*p, eq, changed_leading_term)) {
+                if (try_simplify_using(eq, *p, changed_leading_term)) {
                     simplified = true;
                 }
                 if (canceled() || eq.poly().is_val()) {
@@ -493,7 +507,7 @@ namespace dd {
         for (unsigned i = 0; i < sz; ++i) {
             equation& target = *set[i];
             bool changed_leading_term = false;
-            bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term); 
+            bool simplified = !done() && try_simplify_using(target, eq, changed_leading_term); 
             if (simplified && is_trivial(target)) {
                 retire(&target);
             }
@@ -521,7 +535,7 @@ namespace dd {
       return true if the target was simplified. 
       set changed_leading_term if the target is in the m_processed set and the leading term changed.
      */
-    bool grobner::simplify_source_target(equation const& src, equation& dst, bool& changed_leading_term) {
+    bool grobner::try_simplify_using(equation& dst, equation const& src, bool& changed_leading_term) {
         if (&src == &dst) {
             return false;
         }
@@ -585,7 +599,7 @@ namespace dd {
         if (!simplify_using(m_processed, eq)) return false;
         TRACE("grobner", display(tout << "eq = ", eq););
         superpose(eq);
-        return simplify_to_simplify(eq);
+        return simplify_watch(eq);
     }
 
     void grobner::tuned_init() {
@@ -596,6 +610,7 @@ namespace dd {
             m_level2var[i] = l2v[i];
             m_var2level[l2v[i]] = i;
         }
+        m_watch.reset();
         m_watch.reserve(m_level2var.size());
         m_levelp1 = m_level2var.size();
         for (equation* eq : m_to_simplify) add_to_watch(*eq);
@@ -611,7 +626,7 @@ namespace dd {
         }
     }
 
-    bool grobner::simplify_to_simplify(equation const& eq) {
+    bool grobner::simplify_watch(equation const& eq) {
         unsigned v = eq.poly().var();
         auto& watch = m_watch[v];
         unsigned j = 0;
@@ -620,13 +635,16 @@ namespace dd {
             SASSERT(target.state() == to_simplify);
             SASSERT(target.poly().var() == v);
             bool changed_leading_term = false;
-            if (!done()) simplify_source_target(eq, target, changed_leading_term);
+            if (!done()) {
+                try_simplify_using(target, eq, changed_leading_term);
+            }
             if (is_trivial(target)) {
                 retire(&target);
             }
-            else if (check_conflict(target)) {
-                // pushed to solved
-            } 
+            else if (is_conflict(target)) {
+                pop_equation(target);
+                set_conflict(target);
+            }
             else if (target.poly().var() != v) {
                 // move to other watch list
                 m_watch[target.poly().var()].push_back(_target);
diff --git a/src/math/grobner/pdd_grobner.h b/src/math/grobner/pdd_grobner.h
index 22a480ccf..cc08c363b 100644
--- a/src/math/grobner/pdd_grobner.h
+++ b/src/math/grobner/pdd_grobner.h
@@ -125,16 +125,18 @@ private:
     bool done();
     void superpose(equation const& eq1, equation const& eq2);
     void superpose(equation const& eq);
-    bool simplify_source_target(equation const& source, equation& target, bool& changed_leading_term);
     bool simplify_using(equation& eq, equation_vector const& eqs);
     bool simplify_using(equation_vector& set, equation const& eq);
     void simplify_using(equation & dst, equation const& src, bool& changed_leading_term);
+    bool try_simplify_using(equation& target, equation const& source, bool& changed_leading_term);
 
-    bool eliminate(equation& eq) { return is_trivial(eq) && (del_equation(eq), true); }
     bool is_trivial(equation const& eq) const { return eq.poly().is_zero(); }    
     bool is_simpler(equation const& eq1, equation const& eq2) { return eq1.poly() < eq2.poly(); }
-    bool check_conflict(equation& eq) { return eq.poly().is_val() && !is_trivial(eq) && (set_conflict(eq), true); }    
+    bool is_conflict(equation const* eq) const { return is_conflict(*eq); }
+    bool is_conflict(equation const& eq) const { return eq.poly().is_val() && !is_trivial(eq); }
+    bool check_conflict(equation& eq) { return is_conflict(eq) && (set_conflict(eq), true); }    
     void set_conflict(equation& eq) { m_conflict = &eq; push_equation(solved, eq); }
+    void set_conflict(equation* eq) { m_conflict = eq; push_equation(solved, eq); }
     bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); }
     bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit;  }
 
@@ -147,7 +149,7 @@ private:
     bool tuned_step();
     void tuned_init();
     equation* tuned_pick_next();
-    bool simplify_to_simplify(equation const& eq);
+    bool simplify_watch(equation const& eq);
     void add_to_watch(equation& eq);
 
     void del_equation(equation& eq) { del_equation(&eq); }    
diff --git a/src/test/pdd_grobner.cpp b/src/test/pdd_grobner.cpp
index e7f7c1060..7a60426c1 100644
--- a/src/test/pdd_grobner.cpp
+++ b/src/test/pdd_grobner.cpp
@@ -2,6 +2,7 @@
 #include "math/grobner/pdd_grobner.h"
 
 #include "ast/bv_decl_plugin.h"
+#include "ast/ast_util.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/reg_decl_plugins.h"
@@ -74,6 +75,71 @@ namespace dd {
         // 
     }
 
+    expr_ref elim_or(ast_manager& m, expr* e) {
+        obj_map<expr, expr*> cache;
+        expr_ref_vector trail(m), todo(m), args(m);
+        todo.push_back(e);
+        while (!todo.empty()) {
+            expr* f = todo.back(), *g;
+            
+            if (!is_app(f)) {
+                cache.insert(f, f);
+            }
+
+            if (cache.contains(f)) {
+                todo.pop_back();
+                continue;
+            }
+
+            app* a = to_app(f);
+            args.reset();
+            for (expr* arg : *a) {
+                if (cache.find(arg, g)) {
+                    args.push_back(g);
+                }
+                else {
+                    todo.push_back(arg);
+                }
+            }
+            if (args.size() != a->get_num_args()) {
+                continue;
+            }
+            todo.pop_back();
+            if (m.is_or(a)) {
+                for (unsigned i = 0; i < args.size(); ++i) {
+                    args[i] = mk_not(m, args.get(i));
+                }
+                g = m.mk_not(m.mk_and(args.size(), args.c_ptr()));
+            }
+            else if (m.is_and(a)) {
+                g = m.mk_and(args.size(), args.c_ptr());
+                trail.push_back(g);
+            }
+            else if (m.is_eq(a)) {
+                expr* x = args.get(0);
+                expr* y = args.get(1);
+                if (m.is_not(x, x)) {
+                    g = m.mk_xor(x, y);
+                }
+                else if (m.is_not(y, y)) {
+                    g = m.mk_xor(x, y);
+                }
+                else {
+                    g = m.mk_not(m.mk_xor(x, y));
+                }
+            }
+            else if (m.is_not(a)) {
+                g = mk_not(m, args.get(0));
+            }
+            else {
+                g = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
+            }
+            trail.push_back(g);
+            cache.insert(a, g);
+        }
+        return expr_ref(cache[e], m);
+    }
+
     void add_def(unsigned_vector const& id2var, app* e, ast_manager& m, pdd_manager& p, grobner& g) {
         expr* a, *b;
         pdd v1 = p.mk_var(id2var[e->get_id()]);
@@ -90,17 +156,17 @@ namespace dd {
         }
         else if (m.is_not(e, a)) {
             pdd v2 = p.mk_var(id2var[a->get_id()]);
-            q = v1 + v2 - 1;
+            q = v1 - ~v2;
         }
         else if (m.is_eq(e, a, b)) {
             pdd v2 = p.mk_var(id2var[a->get_id()]);
             pdd v3 = p.mk_var(id2var[b->get_id()]);
-            // v1 = (v2 = v3)
-            // 111, 100 = 0
-            // 001, 010 = 0
-            // 000, 011 = 1
-            // 110, 101 = 1
-            q = v1 - v2 - v3 + 1 + 2*v2*v3 - 2*v1*v2*v3;
+            q = v1 - ~(v2 ^ v3);
+        }
+        else if (m.is_xor(e, a, b)) {
+            pdd v2 = p.mk_var(id2var[a->get_id()]);
+            pdd v3 = p.mk_var(id2var[b->get_id()]);
+            q = v1 - (v2 ^ v3);
         }
         else if (is_uninterp_const(e)) {
             return;
@@ -131,13 +197,18 @@ namespace dd {
         unsigned_vector id2var;
 
         collect_id2var(id2var, fmls);
-        pdd_manager p(id2var.size());
-        if (use_mod2) p.set_mod2_semantics();
+        pdd_manager p(id2var.size(), use_mod2 ? pdd_manager::mod2_e : pdd_manager::zero_one_vars_e);
         grobner g(m.limit(), p);
 
         for (expr* e : subterms(fmls)) {
             add_def(id2var, to_app(e), m, p, g);
         }
+        if (!use_mod2) { // should be built-in 
+            for (expr* e : subterms(fmls)) {
+                pdd v = p.mk_var(id2var[e->get_id()]);
+                g.add(v*v - v);
+            }
+        }
         for (expr* e : fmls) {
             g.add(1 - p.mk_var(id2var[e->get_id()]));
         }
@@ -152,8 +223,8 @@ namespace dd {
         ast_manager m;
         reg_decl_plugins(m);
         bv_util bv(m);
-        expr_ref x(m.mk_const("x", bv.mk_sort(4)), m);
-        expr_ref y(m.mk_const("y", bv.mk_sort(4)), m);
+        expr_ref x(m.mk_const("x", bv.mk_sort(3)), m);
+        expr_ref y(m.mk_const("y", bv.mk_sort(3)), m);
         expr_ref xy(bv.mk_bv_mul(x, y), m);
         expr_ref yx(bv.mk_bv_mul(y, x), m);
         expr_ref eq(m.mk_not(m.mk_eq(xy,yx)), m);
@@ -166,7 +237,7 @@ namespace dd {
 
         expr_ref_vector fmls(m);
         for (unsigned i = 0; i < g->size(); ++i) {
-            fmls.push_back(g->form(i));        
+            fmls.push_back(elim_or(m, g->form(i)));        
         }
         test_simplify(fmls, true);
         test_simplify(fmls, false);