diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index cf5b67793..37c87cd5b 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -241,37 +241,36 @@ struct pb2bv_rewriter::imp {
             m_args(m)
         {}
 
-        br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+        bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
             if (f->get_family_id() == pb.get_family_id()) {
-                mk_pb(f, sz, args, result);
-                ++m_imp.m_num_translated;
-                return BR_DONE;
+                mk_pb(full, f, sz, args, result);
             }
             else if (au.is_le(f) && is_pb(args[0], args[1])) {
-                ++m_imp.m_num_translated;
                 result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
-                return BR_DONE;
             }
             else if (au.is_lt(f) && is_pb(args[0], args[1])) {
-                ++m_imp.m_num_translated;
                 ++m_k;
                 result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
-                return BR_DONE;
             }
             else if (au.is_ge(f) && is_pb(args[1], args[0])) {
-                ++m_imp.m_num_translated;
                 result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
-                return BR_DONE;
             }
             else if (au.is_gt(f) && is_pb(args[1], args[0])) {
-                ++m_imp.m_num_translated;
                 ++m_k;
                 result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
-                return BR_DONE;
             }
             else if (m.is_eq(f) && is_pb(args[0], args[1])) {
-                ++m_imp.m_num_translated;
                 result = mk_le_ge<l_undef>(m_args.size(), m_args.c_ptr(), m_k);
+            }
+            else {
+                return false;
+            }
+            ++m_imp.m_num_translated;
+            return true;
+        }
+
+        br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+            if (mk_app(true, f, sz, args, result)) {
                 return BR_DONE;
             }
             else {
@@ -350,25 +349,25 @@ struct pb2bv_rewriter::imp {
             return false;
         }
 
-        void mk_pb(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+        void mk_pb(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
             SASSERT(f->get_family_id() == pb.get_family_id());
             if (is_or(f)) {
                 result = m.mk_or(sz, args);
             }
             else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) {
-                result = m_sort.le(true, pb.get_k(f).get_unsigned(), sz, args);
+                result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args);
             }
             else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) {
-                result = m_sort.ge(true, pb.get_k(f).get_unsigned(), sz, args);
+                result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
             }
             else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
-                result = m_sort.eq(pb.get_k(f).get_unsigned(), sz, args);
+                result = m_sort.eq(full, pb.get_k(f).get_unsigned(), sz, args);
             }
             else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
-                result = m_sort.le(true, pb.get_k(f).get_unsigned(), sz, args);
+                result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args);
             }
             else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
-                result = m_sort.ge(true, pb.get_k(f).get_unsigned(), sz, args);
+                result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
             }
             else {
                 result = mk_bv(f, sz, args);
@@ -433,9 +432,6 @@ struct pb2bv_rewriter::imp {
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof) {
         m_rw(e, result, result_proof);
     }
-    void assert_expr(expr * e, expr_ref & result, proof_ref & result_proof) {
-        m_rw(e, result, result_proof);
-    }
     void push() {
         m_fresh_lim.push_back(m_fresh.size());
     }
@@ -472,9 +468,6 @@ unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps();
 void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p);  }
 func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; }
 void pb2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
-void pb2bv_rewriter::assert_expr(expr* e, expr_ref & result, proof_ref & result_proof) { 
-    m_imp->assert_expr(e, result, result_proof); 
-}
 void pb2bv_rewriter::push() { m_imp->push(); }
 void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
 void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } 
diff --git a/src/ast/rewriter/pb2bv_rewriter.h b/src/ast/rewriter/pb2bv_rewriter.h
index 569eaf07d..47d8361cb 100644
--- a/src/ast/rewriter/pb2bv_rewriter.h
+++ b/src/ast/rewriter/pb2bv_rewriter.h
@@ -36,7 +36,6 @@ public:
     void cleanup();
     func_decl_ref_vector const& fresh_constants() const;
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
-    void assert_expr(expr* e, expr_ref & result, proof_ref & result_proof);
     void push();
     void pop(unsigned num_scopes);
     void flush_side_constraints(expr_ref_vector& side_constraints);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index f5efed726..d1fae0156 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -34,6 +34,7 @@ Notes:
 #include "bit_blaster_model_converter.h"
 #include "ast_translation.h"
 #include "ast_util.h"
+#include "propagate_values_tactic.h"
 
 // incremental SAT solver.
 class inc_sat_solver : public solver {
@@ -341,6 +342,7 @@ public:
                      mk_max_bv_sharing_tactic(m),
                      mk_bit_blaster_tactic(m, m_bb_rewriter.get()),
                      //mk_aig_tactic(),
+                     //mk_propagate_values_tactic(m, simp2_p),
                      using_params(mk_simplify_tactic(m), simp2_p));
         while (m_bb_rewriter->get_num_scopes() < m_num_scopes) {
             m_bb_rewriter->push();
@@ -377,6 +379,7 @@ private:
         g = m_subgoals[0];
         expr_ref_vector atoms(m);
         TRACE("sat", g->display_with_dependencies(tout););
+        std::cout << "exprs: " << g->num_exprs() << "\n";
         m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
         m_goal2sat.get_interpreted_atoms(atoms);
         if (!atoms.empty()) {
@@ -520,7 +523,7 @@ private:
         }
         dep2asm_t dep2asm;
         goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
-        for (unsigned i = 0 ; i < m_fmls.size(); ++i) {
+        for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) {
             g->assert_expr(m_fmls[i].get());
         }
         lbool res = internalize_goal(g, dep2asm);
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index 0b136dda7..b6c85c159 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -303,6 +303,7 @@ private:
             }
         }
         m_assertions.reset();
+        m_rewriter.reset();
     }
 };
 
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index e89f9d188..f3288d8d6 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -99,7 +99,6 @@ public:
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
     
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
-
         datatype_util dt(m);
         bv_util bv(m);
         expr_ref_vector bvars(m), conseq(m), bounds(m);
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index d1826e61d..bfd533e8a 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -113,7 +113,7 @@ private:
         expr_ref fml(m);
         expr_ref_vector fmls(m);
         for (unsigned i = 0; i < m_assertions.size(); ++i) {
-            m_rewriter.assert_expr(m_assertions[i].get(), fml, proof);
+            m_rewriter(m_assertions[i].get(), fml, proof);
             m_solver->assert_expr(fml);
         }
         m_rewriter.flush_side_constraints(fmls);
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index 33c4f8b61..87d8bbf3f 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -24,7 +24,6 @@ Notes:
 #ifndef SORTING_NETWORK_H_
 #define SORTING_NETWORK_H_
 
-
     template <typename Ext>
     class sorting_network {
         typedef typename Ext::vector vect;
@@ -213,17 +212,17 @@ Notes:
             }
         }
 
-        literal eq(unsigned k, unsigned n, literal const* xs) {
+        literal eq(bool full, unsigned k, unsigned n, literal const* xs) {
             if (k > n) {
                 return ctx.mk_false();
             }
             SASSERT(k <= n);
             literal_vector in, out;
             if (dualize(k, n, xs, in)) {
-                return eq(k, n, in.c_ptr());
+                return eq(full, k, n, in.c_ptr());
             }
             else if (k == 1) {
-                return mk_exactly_1(true, n, xs);
+                return mk_exactly_1(full, n, xs);
             }
             else {
                 SASSERT(2*k <= n);
@@ -242,34 +241,64 @@ Notes:
         
     private:
 
-
-        literal mk_and(literal l1, literal l2) {
-            literal result = fresh();
-            add_clause(ctx.mk_not(result), l1);
-            add_clause(ctx.mk_not(result), l2);
-            add_clause(ctx.mk_not(l1), ctx.mk_not(l2), result);
-            return result;
-        }
-
-        void mk_implies_or(literal l, unsigned n, literal const* xs) {
+        void add_implies_or(literal l, unsigned n, literal const* xs) {
             literal_vector lits(n, xs);
             lits.push_back(ctx.mk_not(l));
             add_clause(lits);
         }
 
-        void mk_or_implies(literal l, unsigned n, literal const* xs) {
+        void add_or_implies(literal l, unsigned n, literal const* xs) {
             for (unsigned j = 0; j < n; ++j) {
                 add_clause(ctx.mk_not(xs[j]), l);
             }
         }
 
-        literal mk_or(literal_vector const& ors) {
-            if (ors.size() == 1) {
+        literal mk_or(unsigned n, literal const* ors) {
+            if (n == 1) {
                 return ors[0];
             }
             literal result = fresh();
-            mk_implies_or(result, ors.size(), ors.c_ptr());
-            mk_or_implies(result, ors.size(), ors.c_ptr());
+            add_implies_or(result, n, ors);
+            add_or_implies(result, n, ors);
+            return result;
+        }
+
+        literal mk_or(literal l1, literal l2) {
+            literal ors[2] = { l1, l2 };
+            return mk_or(2, ors);
+        }
+        literal mk_or(literal_vector const& ors) {
+            return mk_or(ors.size(), ors.c_ptr());
+        }
+
+        void add_implies_and(literal l, literal_vector const& xs) {
+            for (unsigned j = 0; j < xs.size(); ++j) {
+                add_clause(ctx.mk_not(l), xs[j]);
+            }
+        }
+
+        void add_and_implies(literal l, literal_vector const& xs) {
+            literal_vector lits;
+            for (unsigned j = 0; j < xs.size(); ++j) {
+                lits.push_back(ctx.mk_not(xs[j]));
+            }
+            lits.push_back(l);
+            add_clause(lits);
+        }
+
+        literal mk_and(literal l1, literal l2) {
+            literal_vector xs;
+            xs.push_back(l1); xs.push_back(l2);
+            return mk_and(xs);
+        }
+
+        literal mk_and(literal_vector const& ands) {
+            if (ands.size() == 1) {
+                return ands[0];
+            }
+            literal result = fresh();
+            add_implies_and(result, ands);
+            add_and_implies(result, ands);
             return result;
         }
 
@@ -281,18 +310,19 @@ Notes:
                 r1 = mk_and(r1, mk_or(ors));
             }
             else {
-                mk_implies_or(r1, ors.size(), ors.c_ptr());
+                add_implies_or(r1, ors.size(), ors.c_ptr());
             }
             return r1;
         }
 
+#if 1
         literal mk_at_most_1(bool full, unsigned n, literal const* xs, literal_vector& ors) {
             TRACE("pb", tout << (full?"full":"partial") << " ";
                   for (unsigned i = 0; i < n; ++i) tout << xs[i] << " ";
                   tout << "\n";);
 
-            if (false && !full && n >= 4) {
-                return mk_at_most_1_bimander(n, xs);
+            if (n >= 4 && false) {
+                return mk_at_most_1_bimander(full, n, xs, ors);
             }
             literal_vector in(n, xs);
             literal result = fresh();
@@ -301,17 +331,14 @@ Notes:
             ands.push_back(result);
             while (!in.empty()) {
                 ors.reset();
-                unsigned i = 0;
                 unsigned n = in.size();
                 if (n + 1 == inc_size) ++inc_size;
-                bool last = n <= inc_size;
-                for (; i + inc_size < n; i += inc_size) {                    
-                    mk_at_most_1_small(full, last, inc_size, in.c_ptr() + i, result, ands, ors);
+                for (unsigned i = 0; i < n; i += inc_size) {       
+                    unsigned inc = std::min(n - i, inc_size);
+                    mk_at_most_1_small(full, inc, in.c_ptr() + i, result, ands);
+                    ors.push_back(mk_or(inc, in.c_ptr() + i));
                 }
-                if (i < n) {
-                    mk_at_most_1_small(full, last, n - i, in.c_ptr() + i, result, ands, ors);
-                }
-                if (last) {
+                if (n <= inc_size) {
                     break;
                 }
                 in.reset();
@@ -322,19 +349,40 @@ Notes:
             }
             return result;
         }
+#else
+        literal mk_at_most_1(bool full, unsigned n, literal const* xs, literal_vector& ors) {
+            TRACE("pb", tout << (full?"full":"partial") << " ";
+                  for (unsigned i = 0; i < n; ++i) tout << xs[i] << " ";
+                  tout << "\n";);
 
-        void mk_at_most_1_small(bool full, bool last, unsigned n, literal const* xs, literal result, literal_vector& ands, literal_vector& ors) {
+            literal_vector in(n, xs);
+            unsigned inc_size = 4;
+            literal_vector ands;
+            while (!in.empty()) {
+                ors.reset();
+                unsigned i = 0;
+                unsigned n = in.size();
+                if (n + 1 == inc_size) ++inc_size;
+                for (; i < n; i += inc_size) {                    
+                    unsigned inc = std::min(inc_size, n - i);
+                    ands.push_back(mk_at_most_1_small(inc, in.c_ptr() + i));
+                    ors.push_back(mk_or(inc, in.c_ptr() + i));
+                }
+                if (n <= inc_size) {
+                    break;
+                }
+                in.reset();
+                in.append(ors);
+            }
+            return mk_and(ands);
+        }
+
+#endif
+        void mk_at_most_1_small(bool full, unsigned n, literal const* xs, literal result, literal_vector& ands) {
             SASSERT(n > 0);
             if (n == 1) {
-                ors.push_back(xs[0]);                
                 return;
             }
-            literal ex = fresh();
-            mk_or_implies(ex, n, xs);
-            if (full) {
-                mk_implies_or(ex, n, xs);
-            }
-            ors.push_back(ex);                
             
             // result => xs[0] + ... + xs[n-1] <= 1
             for (unsigned i = 0; i < n; ++i) {
@@ -358,19 +406,75 @@ Notes:
             }
         }
 
-        literal mk_at_most_1_bimander(unsigned n, literal const* xs) {
+        literal mk_at_most_1_small(unsigned n, literal const* xs) {
+            SASSERT(n > 0);
+            if (n == 1) {
+                return ctx.mk_true();
+            }
+
+            
+#if 0
+            literal result = fresh();
+
+            // result => xs[0] + ... + xs[n-1] <= 1
+            for (unsigned i = 0; i < n; ++i) {
+                for (unsigned j = i + 1; j < n; ++j) {
+                    add_clause(ctx.mk_not(result), ctx.mk_not(xs[i]), ctx.mk_not(xs[j]));
+                }
+            }            
+
+            // xs[0] + ... + xs[n-1] <= 1 => result
+            for (unsigned i = 0; i < n; ++i) {
+                literal_vector lits;
+                lits.push_back(result);
+                for (unsigned j = 0; j < n; ++j) {
+                    if (j != i) lits.push_back(xs[j]);
+                }
+                add_clause(lits);
+            }
+
+            return result;
+#endif
+#if 1
+            // r <=> and( or(!xi,!xj))
+            // 
+            literal_vector ands;
+            for (unsigned i = 0; i < n; ++i) {
+                for (unsigned j = i + 1; j < n; ++j) {
+                    ands.push_back(mk_or(ctx.mk_not(xs[i]), ctx.mk_not(xs[j])));
+                }                
+            }
+            return mk_and(ands);
+#else
+            // r <=> or (and !x_{j != i})
+
+            literal_vector ors;
+            for (unsigned i = 0; i < n; ++i) {
+                literal_vector ands;
+                for (unsigned j = 0; j < n; ++j) {
+                    if (j != i) {
+                        ands.push_back(ctx.mk_not(xs[j]));
+                    }
+                }                
+                ors.push_back(mk_and(ands));
+            }
+            return mk_or(ors);
+            
+#endif
+        }
+
+        
+        // 
+
+        literal mk_at_most_1_bimander(bool full, unsigned n, literal const* xs, literal_vector& ors) {
             literal_vector in(n, xs);
             literal result = fresh();
             unsigned inc_size = 2;
-            bool last = false;
-            bool full = false;
-            literal_vector ors, ands;
-            unsigned i = 0;
-            for (; i + inc_size < n; i += inc_size) {                    
-                mk_at_most_1_small(full, last, inc_size, in.c_ptr() + i, result, ands, ors);
-            }
-            if (i < n) {
-                mk_at_most_1_small(full, last, n - i, in.c_ptr() + i, result, ands, ors);
+            literal_vector ands;
+            for (unsigned i = 0; i < n; i += inc_size) {                    
+                unsigned inc = std::min(n - i, inc_size);
+                mk_at_most_1_small(full, inc, in.c_ptr() + i, result, ands);
+                ors.push_back(mk_or(inc, in.c_ptr() + i));
             }
             
             unsigned nbits = 0;
@@ -381,7 +485,7 @@ Notes:
             for (unsigned k = 0; k < nbits; ++k) {
                 bits.push_back(fresh());
             }
-            for (i = 0; i < ors.size(); ++i) {
+            for (unsigned i = 0; i < ors.size(); ++i) {
                 for (unsigned k = 0; k < nbits; ++k) {
                     bool bit_set = (i & (static_cast<unsigned>(1 << k))) != 0;
                     add_clause(ctx.mk_not(result), ctx.mk_not(ors[i]), bit_set ? bits[k] : ctx.mk_not(bits[k]));