diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 68f7596ee..0915ae1b6 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2058,6 +2058,22 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
     return r;
 }
 
+expr* ast_manager::mk_or_reduced(unsigned n, expr* const* args) {
+    switch (n) {
+    case 0: return mk_false();
+    case 1: return args[0];
+    default: return mk_or(n, args);
+    }
+}
+
+expr* ast_manager::mk_and_reduced(unsigned n, expr* const* args) {
+    switch (n) {
+    case 0: return mk_true();
+    case 1: return args[0];
+    default: return mk_and(n, args);
+    }
+}
+
 func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const & suffix, unsigned arity, 
                                             sort * const * domain, sort * range) {
     func_decl_info info(null_family_id, null_decl_kind);
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 68f08e1ac..f8ba43554 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2004,6 +2004,9 @@ public:
     app * mk_true() { return m_true; }
     app * mk_false() { return m_false; }
     app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
+    expr * mk_or_reduced(unsigned num_args, expr * const * args);
+    expr * mk_and_reduced(unsigned num_args, expr * const * args);
+
 
     func_decl* mk_and_decl() { 
         sort* domain[2] = { m_bool_sort, m_bool_sort };
diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index 0cfe1c096..36103c4f0 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -271,3 +271,12 @@ rational pb_util::to_rational(parameter const& p) const {
     SASSERT(p.is_rational());
     return p.get_rational();
 }
+
+bool pb_util::has_unit_coefficients(func_decl* f) const {
+    if (is_at_most_k(f) || is_at_least_k(f)) return true;
+    unsigned sz = f->get_arity();
+    for (unsigned i = 0; i < sz; ++i) {
+        if (!get_coeff(f, i).is_one()) return false;
+    }
+    return true;
+}
diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h
index 8ecf0f259..0bc8eab17 100644
--- a/src/ast/pb_decl_plugin.h
+++ b/src/ast/pb_decl_plugin.h
@@ -103,6 +103,9 @@ public:
     bool is_ge(expr* a, rational& k) const;
     rational get_coeff(expr* a, unsigned index) const { return get_coeff(to_app(a)->get_decl(), index); }
     rational get_coeff(func_decl* a, unsigned index) const; 
+    bool has_unit_coefficients(func_decl* f) const;
+    bool has_unit_coefficients(expr* f) const { return is_app(f) && has_unit_coefficients(to_app(f)->get_decl()); }
+
 
     bool is_eq(func_decl* f) const;
     bool is_eq(expr* e) const { return is_app(e) && is_eq(to_app(e)->get_decl()); }
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index f879c8934..48dbb410b 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -397,8 +397,12 @@ public:
                 */
                 sort_assumptions(asms);            
                 unsigned index = 0;
+                unsigned last_index = 0;
                 while (index < asms.size() && is_sat != l_false) {
-                    index = next_index(asms, index);
+                    while (asms.size() > 10*(index - last_index) && index < asms.size()) {
+                        index = next_index(asms, index);
+                    }
+                    last_index = index;
                     is_sat = s().check_sat(index, asms.c_ptr());
                 }            
             }
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 27185228d..ca4b40740 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -69,7 +69,6 @@ namespace opt {
         m_objectives_lim.pop_back();            
         m_hard_lim.pop_back();   
     }
-
     
     void context::scoped_state::add(expr* hard) {
         m_hard.push_back(hard);
@@ -608,7 +607,7 @@ namespace opt {
             for (unsigned i = 0; i < a->get_num_args(); ++i) {
                 expr* arg = a->get_arg(i);
                 if (m.is_true(arg)) {
-
+                    // skip
                 }
                 else if (m.is_false(arg)) {
                     offset += m_objectives[index].m_weights[i];
@@ -764,8 +763,8 @@ namespace opt {
                 SASSERT(obj.m_id == id);
                 obj.m_terms.reset();
                 obj.m_terms.append(terms);
-                obj.m_offset = offset;
-                obj.m_neg = neg;
+                obj.m_adjust_bound.set_offset(offset);
+                obj.m_adjust_bound.set_negate(neg);
                 TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";);
             }
             else if (is_maximize(fml, tr, orig_term, index)) {
@@ -835,23 +834,23 @@ namespace opt {
             switch(obj.m_type) {
             case O_MINIMIZE:
                 if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
-                    r += obj.m_offset;
+                    inf_eps val = obj.m_adjust_bound.neg_add(r);
                     if (is_lower) {
-                        m_optsmt.update_lower(obj.m_index, inf_eps(-r), override);
+                        m_optsmt.update_lower(obj.m_index, val, override);
                     }
                     else {
-                        m_optsmt.update_upper(obj.m_index, inf_eps(-r), override);
+                        m_optsmt.update_upper(obj.m_index, val, override);
                     }
                 }
                 break;
             case O_MAXIMIZE:
                 if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
-                    r += obj.m_offset;
+                    inf_eps val = obj.m_adjust_bound.neg_add(r);
                     if (is_lower) {
-                        m_optsmt.update_lower(obj.m_index, inf_eps(r), override);
+                        m_optsmt.update_lower(obj.m_index, val, override);
                     }
                     else {
-                        m_optsmt.update_upper(obj.m_index, inf_eps(r), override);
+                        m_optsmt.update_upper(obj.m_index, val, override);
                     }
                 }
                 break;
@@ -921,10 +920,7 @@ namespace opt {
         switch(obj.m_type) {
         case O_MAXSMT: {
             rational r = m_maxsmts.find(obj.m_id)->get_lower();
-            TRACE("opt", tout << "maxsmt: " << r << " negate: " << obj.m_neg << " offset: " << obj.m_offset << "\n";);
-            if (obj.m_neg) r.neg();
-            r += obj.m_offset;
-            return inf_eps(r);
+            return obj.m_adjust_bound.neg_add(r);
         }
         case O_MINIMIZE:
             return -m_optsmt.get_upper(obj.m_index);
@@ -942,13 +938,9 @@ namespace opt {
         }
         objective const& obj = m_objectives[idx];
         switch(obj.m_type) {
-        case O_MAXSMT: {
-            rational r = m_maxsmts.find(obj.m_id)->get_upper();
-            TRACE("opt", tout << "maxsmt: " << r << " negate: " << obj.m_neg << " offset: " << obj.m_offset << "\n";);
-            if (obj.m_neg) r.neg();
-            r += obj.m_offset;
-            return inf_eps(r);
-        }
+        case O_MAXSMT: 
+            return obj.m_adjust_bound.neg_add(m_maxsmts.find(obj.m_id)->get_upper());
+            // TBD: adjust bound
         case O_MINIMIZE:
             return -m_optsmt.get_lower(obj.m_index);
         case O_MAXIMIZE: 
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 09ddb725a..051729aff 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -51,8 +51,7 @@ namespace opt {
             app_ref     m_term;          // for maximize, minimize term
             expr_ref_vector   m_terms;   // for maxsmt
             vector<rational>  m_weights; // for maxsmt
-            rational          m_offset;  // for maxsmt
-            bool              m_neg;     // negate
+            bound_adjustment  m_adjust_bound;
             symbol      m_id;            // for maxsmt
             unsigned    m_index;         // for maximize/minimize index
 
@@ -60,18 +59,18 @@ namespace opt {
                 m_type(is_max?O_MAXIMIZE:O_MINIMIZE),
                 m_term(t),
                 m_terms(t.get_manager()),
-                m_offset(0),
-                m_neg(false),
                 m_id(),
                 m_index(idx)
-            {}
+            {
+                if (!is_max) {
+                    m_adjust_bound.set_negate(true);
+                }
+            }
 
             objective(ast_manager& m, symbol id):
                 m_type(O_MAXSMT),
                 m_term(m),
                 m_terms(m),
-                m_offset(0),
-                m_neg(false),
                 m_id(id),
                 m_index(0)
             {}
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 07f2e756b..0e59a9eb9 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -36,6 +36,33 @@ namespace opt {
 
     typedef inf_eps_rational<inf_rational> inf_eps;
 
+    // Adjust bound bound |-> (m_negate?-1:1)*(m_offset + bound)
+    class bound_adjustment {
+        rational m_offset;
+        bool     m_negate;
+    public:
+        bound_adjustment(rational const& offset, bool neg):
+            m_offset(offset),
+            m_negate(neg)
+        {}
+        bound_adjustment(): m_offset(0), m_negate(false) {}
+        void set_offset(rational const& o) { m_offset = o; }
+        void set_negate(bool neg) { m_negate = neg; }
+        rational const& get_offset() const { return m_offset; }
+        bool get_negate() { return m_negate; }
+        inf_eps add_neg(rational const& r) const {
+            rational result = r + m_offset;
+            if (m_negate) result.neg();
+            return inf_eps(result);
+        }
+        inf_eps neg_add(rational const& r) const {
+            rational result = r;
+            if (m_negate) result.neg();
+            result += m_offset;
+            return inf_eps(result);
+        }
+    };
+
 
     class opt_solver : public solver_na2as {
     private:
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index f5f446095..3d95f1c72 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -958,7 +958,7 @@ namespace smt {
             typename atoms::iterator lo_inf1 = begin1, lo_sup1 = begin1;
             typename atoms::iterator hi_inf1 = begin2, hi_sup1 = begin2;
             bool flo_inf, fhi_inf, flo_sup, fhi_sup;
-            //std::cout << atoms.size() << "\n";
+   //         std::cout << atoms.size() << "\n";
             ptr_addr_hashtable<typename atom> visited;
             for (unsigned i = 0; i < atoms.size(); ++i) {
                 atom* a1 = atoms[i];
@@ -966,8 +966,8 @@ namespace smt {
                 hi_inf1 = next_inf(a1, A_UPPER, hi_inf, end, fhi_inf);
                 lo_sup1 = next_sup(a1, A_LOWER, lo_sup, end, flo_sup);
                 hi_sup1 = next_sup(a1, A_UPPER, hi_sup, end, fhi_sup);
-                //std::cout << "v" << a1->get_var() << ((a1->get_atom_kind()==A_LOWER)?" <= ":" >= ") << a1->get_k() << "\n";
-                //std::cout << (lo_inf1 != end) << " " << (lo_sup1 != end) << " " << (hi_inf1 != end) << " " << (hi_sup1 != end) << "\n";
+//                std::cout << "v" << a1->get_var() << ((a1->get_atom_kind()==A_LOWER)?" <= ":" >= ") << a1->get_k() << "\n";
+ //               std::cout << (lo_inf1 != end) << " " << (lo_sup1 != end) << " " << (hi_inf1 != end) << " " << (hi_sup1 != end) << "\n";
                 if (lo_inf1 != end) lo_inf = lo_inf1; 
                 if (lo_sup1 != end) lo_sup = lo_sup1; 
                 if (hi_inf1 != end) hi_inf = hi_inf1; 
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 7570a73c5..b8a5e7bd1 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1156,7 +1156,7 @@ namespace smt {
             return literal(ctx.mk_bool_var(y));
         }
         
-        literal max(literal a, literal b) {
+        literal mk_max(literal a, literal b) {
             if (a == b) return a;
             expr_ref t1(m), t2(m), t3(m);
             ctx.literal2expr(a, t1);
@@ -1166,7 +1166,7 @@ namespace smt {
             return literal(v);
         }
 
-        literal min(literal a, literal b) {
+        literal mk_min(literal a, literal b) {
             if (a == b) return a;
             expr_ref t1(m), t2(m), t3(m);
             ctx.literal2expr(a, t1);
@@ -1176,6 +1176,8 @@ namespace smt {
             return literal(v);
         }
 
+        literal mk_not(literal a) { return ~a; }
+
         void mk_clause(unsigned n, literal const* ls) {
             literal_vector tmp(n, ls);
             ctx.mk_clause(n, tmp.c_ptr(), 0, CLS_AUX, 0);
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index 55f50fbb2..3d112e36f 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -39,8 +39,55 @@ namespace pb {
         m(m),
         au(m),
         pb(m),
-        bv(m)
+        bv(m),
+        m_sort(*this),
+        m_lemmas(m),
+        m_trail(m)
     {}
+
+    void card2bv_rewriter::mk_assert(func_decl * f, unsigned sz, expr * const* args, expr_ref & result, expr_ref_vector& lemmas) {
+        m_lemmas.reset();
+        SASSERT(f->get_family_id() == pb.get_family_id());
+        if (is_or(f)) {
+            result = m.mk_or(sz, args);
+        }
+        else if (is_and(f)) {
+            result = m.mk_and(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);
+        }
+        else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
+            result = m_sort.le(false, 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(false, pb.get_k(f).get_unsigned(), sz, args);
+        }
+        else {
+            br_status st = mk_shannon(f, sz, args, result);
+            if (st == BR_FAILED) {
+                mk_bv(f, sz, args, result);
+            }
+        }
+        lemmas.append(m_lemmas);
+    }
+    
+    std::ostream& card2bv_rewriter::pp(std::ostream& out, literal lit) {
+        return out << mk_ismt2_pp(lit, m);
+    }
+
+    card2bv_rewriter::literal card2bv_rewriter::trail(literal l) {
+        m_trail.push_back(l);
+        return l;
+    }
+    card2bv_rewriter::literal card2bv_rewriter::fresh() {
+        return trail(m.mk_fresh_const("sn", m.mk_bool_sort()));
+    }
+
+    void card2bv_rewriter::mk_clause(unsigned n, literal const* lits) {
+        m_lemmas.push_back(m.mk_or_reduced(n, lits));
+    }
+
     
     br_status card2bv_rewriter::mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
         if (f->get_family_id() == null_family_id) {
@@ -69,7 +116,8 @@ namespace pb {
             }
             br_status st = mk_shannon(f, sz, args, result);
             if (st == BR_FAILED) {
-                return mk_bv(f, sz, args, result);
+                mk_bv(f, sz, args, result);
+                return BR_DONE;
             }
             else {
                 return st;
@@ -135,7 +183,7 @@ namespace pb {
         return false;
     }
 
-    br_status card2bv_rewriter::mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+    void card2bv_rewriter::mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
         expr_ref zero(m), a(m), b(m);
         expr_ref_vector es(m);
         unsigned bw = get_num_bits(f);        
@@ -172,7 +220,6 @@ namespace pb {
         default:
             UNREACHABLE();
         }
-        return BR_DONE;
     }
 
     struct argc_t {
@@ -352,10 +399,30 @@ namespace pb {
         if (m.is_true(lo)) return m.mk_implies(c, hi);
         return m.mk_ite(c, hi, lo);
     }
+
+    void card_pb_rewriter::rewrite(expr* e, expr_ref& result) {
+        if (pb.is_eq(e)) {
+            app* a = to_app(e);
+            ast_manager& m = m_lemmas.get_manager();
+            unsigned sz = a->get_num_args();
+            expr_ref_vector args(m);
+            expr_ref tmp(m);
+            for (unsigned i = 0; i < sz; ++i) {
+                (*this)(a->get_arg(i), tmp);
+                args.push_back(tmp);
+            }
+            m_cfg.m_r.mk_assert(a->get_decl(), sz, args.c_ptr(), result, m_lemmas);
+        }
+        else {
+            (*this)(e, result);    
+        }
+    }
+
 };
 
 template class rewriter_tpl<pb::card2bv_rewriter_cfg>;
 
+
 class card2bv_tactic : public tactic {
     ast_manager &              m;
     params_ref                 m_params;
@@ -402,6 +469,7 @@ public:
         tactic_report report("card2bv", *g);
         m_rw1.reset(); 
         m_rw2.reset(); 
+        m_rw2.lemmas().reset();
         
         if (g->inconsistent()) {
             result.push_back(g.get());
@@ -413,9 +481,12 @@ public:
         for (unsigned idx = 0; idx < size; idx++) {
             m_rw1(g->form(idx), new_f1);
             TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;);
-            m_rw2(new_f1, new_f2);
+            m_rw2.rewrite(new_f1, new_f2);
             g->update(idx, new_f2, g->pr(idx), g->dep(idx));
         }
+        for (unsigned i = 0; i < m_rw2.lemmas().size(); ++i) {
+            g->assert_expr(m_rw2.lemmas()[i].get());
+        }
 
         g->inc_depth();
         result.push_back(g.get());
diff --git a/src/tactic/arith/card2bv_tactic.h b/src/tactic/arith/card2bv_tactic.h
index 925e6d0d2..ed96376b5 100644
--- a/src/tactic/arith/card2bv_tactic.h
+++ b/src/tactic/arith/card2bv_tactic.h
@@ -23,6 +23,9 @@ Notes:
 #include"pb_decl_plugin.h"
 #include"th_rewriter.h"
 #include"rewriter.h"
+#include<typeinfo>
+#include"sorting_network.h"
+
 
 class ast_manager;
 class tactic;
@@ -30,12 +33,20 @@ class tactic;
 namespace pb {
 
     class card2bv_rewriter {
+    public:
+        typedef expr* literal;
+        typedef ptr_vector<expr> literal_vector;
+    private:
         ast_manager& m;
         arith_util   au;
         pb_util      pb;
         bv_util      bv;
+        psort_nw<card2bv_rewriter> m_sort;
+        expr_ref_vector m_lemmas;
+        expr_ref_vector m_trail;
+
         unsigned get_num_bits(func_decl* f);
-        br_status mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
+        void mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
         br_status mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
         expr* negate(expr* e);
         expr* mk_ite(expr* c, expr* hi, expr* lo);
@@ -45,6 +56,19 @@ namespace pb {
     public:
         card2bv_rewriter(ast_manager& m);
         br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
+        void mk_assert(func_decl * f, unsigned sz, expr * const* args, expr_ref & result, expr_ref_vector& lemmas);
+
+        // definitions used for sorting network
+        literal mk_false() { return m.mk_false(); }
+        literal mk_true() { return m.mk_true(); }
+        literal mk_max(literal a, literal b) { return trail(m.mk_or(a, b)); }
+        literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); }
+        literal mk_not(literal a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); }
+        std::ostream& pp(std::ostream& out, literal lit);
+        literal fresh();
+        literal trail(literal l);
+        void mk_clause(unsigned n, literal const* lits);
+        
     };
 
     struct card2bv_rewriter_cfg : public default_rewriter_cfg {
@@ -55,15 +79,23 @@ namespace pb {
             result_pr = 0;
             return m_r.mk_app_core(f, num, args, result);
         }
-    card2bv_rewriter_cfg(ast_manager & m):m_r(m) {}
+        card2bv_rewriter_cfg(ast_manager & m):m_r(m) {}
     };
     
     class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
         card2bv_rewriter_cfg m_cfg;
+        pb_util         pb;
+        expr_ref_vector m_lemmas;
     public:
-    card_pb_rewriter(ast_manager & m):
-        rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
-            m_cfg(m) {}
+        card_pb_rewriter(ast_manager & m):
+            rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
+            m_cfg(m),
+            pb(m),
+            m_lemmas(m) {}
+        
+        void rewrite(expr* e, expr_ref& result);
+
+        expr_ref_vector& lemmas() { return m_lemmas; }
     };
 };
 
diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp
index 60af1eae8..6fdfb1560 100644
--- a/src/test/hilbert_basis.cpp
+++ b/src/test/hilbert_basis.cpp
@@ -556,7 +556,7 @@ static void test_A_5_5_3() {
         for (unsigned k = 1; k <= 5; ++k) {
             for (unsigned l = 1; l <= 5; ++l) {
                 for (unsigned j = 1; j <= 3; ++j) {
-                    bool one = ((j*k <= i) && (((i - j) % 3) == 0); // fixme
+                    bool one = ((j*k <= i) && (((i - j) % 3) == 0)); // fixme
                     v.push_back(rational(one));
                 }
             }
diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp
index 5ae6362b1..8792a4795 100644
--- a/src/test/sorting_network.cpp
+++ b/src/test/sorting_network.cpp
@@ -1,9 +1,13 @@
-
-#include "sorting_network.h"
+#include "trace.h"
 #include "vector.h"
 #include "ast.h"
 #include "ast_pp.h"
 #include "reg_decl_plugins.h"
+#include "sorting_network.h"
+#include "smt_kernel.h"
+#include "model_smt2_pp.h"
+#include "smt_params.h"
+
 
 
 struct ast_ext {
@@ -26,6 +30,8 @@ struct ast_ext {
     }        
 };
 
+
+
 struct unsigned_ext {
     unsigned_ext() {}
     typedef unsigned T;
@@ -41,6 +47,7 @@ struct unsigned_ext {
     }
 };
 
+
 static void is_sorted(svector<unsigned> const& v) {
     for (unsigned i = 0; i + 1 < v.size(); ++i) {
         SASSERT(v[i] <= v[i+1]);
@@ -134,9 +141,97 @@ void test_sorting3() {
     }
 }
 
+
+struct ast_ext2 {
+    ast_manager& m;
+    expr_ref_vector m_clauses;
+    expr_ref_vector m_trail;
+    ast_ext2(ast_manager& m):m(m), m_clauses(m), m_trail(m) {}
+    typedef expr* literal;
+    typedef ptr_vector<expr> literal_vector;
+
+    expr* trail(expr* e) {
+        m_trail.push_back(e);
+        return e;
+    }
+
+    literal mk_false() { return m.mk_false(); }
+    literal mk_true() { return m.mk_true(); }
+    literal mk_max(literal a, literal b) { 
+        return trail(m.mk_or(a, b)); 
+    }
+    literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); }
+    literal mk_not(literal a) { if (m.is_not(a,a)) return a; 
+        return trail(m.mk_not(a)); 
+    }
+    std::ostream& pp(std::ostream& out, literal lit) {
+        return out << mk_pp(lit, m);
+    }
+    literal fresh() { 
+        return trail(m.mk_fresh_const("x", m.mk_bool_sort()));
+    }
+    void mk_clause(unsigned n, literal const* lits) {
+        m_clauses.push_back(m.mk_or_reduced(n, lits));
+    }
+};
+
+
+void test_sorting5(unsigned n, unsigned k) {
+    std::cout << "n: " << n << " k: " << k << "\n";
+    SASSERT(k < n);
+    ast_manager m;
+    reg_decl_plugins(m);
+    ast_ext2 ext(m);
+    expr_ref_vector in(m), out(m);
+    for (unsigned i = 0; i < n; ++i) {
+        in.push_back(m.mk_fresh_const("a",m.mk_bool_sort()));
+    }
+    smt_params fp;
+    smt::kernel solver(m, fp);
+    psort_nw<ast_ext2> sn(ext);
+    expr_ref result(m);
+    result = sn.eq(k, in.size(), in.c_ptr());
+    solver.assert_expr(result);
+    for (unsigned i = 0; i < ext.m_clauses.size(); ++i) {
+        solver.assert_expr(ext.m_clauses[i].get());
+    }
+    lbool res = solver.check();
+    SASSERT(res == l_true);
+    std::cout << res << "\n";
+
+    solver.push();
+    for (unsigned i = 0; i < k; ++i) {
+        solver.assert_expr(in[i].get());        
+    }
+    res = solver.check();
+    SASSERT(res == l_true);
+    solver.assert_expr(in[k].get());
+    res = solver.check();
+    if (res == l_true) {
+        TRACE("pb",
+              unsigned sz = solver.size();
+              for (unsigned i = 0; i < sz; ++i) {
+                  tout << mk_pp(solver.get_formulas()[i], m) << "\n";
+              });
+        model_ref model;
+        solver.get_model(model);
+        model_smt2_pp(std::cout, m, *model, 0);
+        TRACE("pb", model_smt2_pp(tout, m, *model, 0););
+    }
+    SASSERT(res == l_false);
+    solver.pop(1);
+
+}
+
 void tst_sorting_network() {
     test_sorting1();
     test_sorting2();
     test_sorting3();
     test_sorting4();
+    test_sorting5(7,6);
+    for (unsigned n = 3; n < 10; n += 2) {
+        for (unsigned k = 1; k < n; ++k) {
+            test_sorting5(n, k);
+        }
+    }
 }
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index f403f9e16..c2bdc600e 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -144,7 +144,7 @@ Notes:
             }
         };
 
-        static vc min(vc const& v1, vc const& v2) {
+        static vc mk_min(vc const& v1, vc const& v2) {
             return (v1.to_int() < v2.to_int())?v1:v2;
         }
 
@@ -205,7 +205,7 @@ Notes:
                 SASSERT(2*k <= n);
                 m_t = full?LE_FULL:LE;
                 card(k + 1, n, xs, out);
-                return ~out[k]; 
+                return ctx.mk_not(out[k]); 
             }
         }
 
@@ -219,11 +219,11 @@ Notes:
                 return eq(k, n, in.c_ptr());
             }
             else {
-                SASSERT(2*k < n);
+                SASSERT(2*k <= n);
                 m_t = EQ;
                 card(k+1, n, xs, out);
                 SASSERT(out.size() >= k+1);
-                return out[k-1]; // & ~out[m] TBD
+                return ctx.mk_min(out[k-1], ctx.mk_not(out[k]));
             }
         }
 
@@ -253,10 +253,10 @@ Notes:
             }
             k = N - k;
             for (unsigned i = 0; i < N; ++i) {
-                in.push_back(~xs[i]);
+                in.push_back(ctx.mk_not(xs[i]));
             }
             TRACE("pb", 
-                  pp(tout << N << ": ", in);
+                  pp(tout << N << ": ", in);                  
                   tout << " ~ " << k << "\n";);
             return true;
         }
@@ -269,16 +269,16 @@ Notes:
         unsigned power2(unsigned n) const { SASSERT(n < 10); return 1 << n; }
 
 
-        literal max(literal a, literal b) {
+        literal mk_max(literal a, literal b) {
             if (a == b) return a;
             m_stats.m_num_compiled_vars++;
-            return ctx.max(a, b);
+            return ctx.mk_max(a, b);
         }
 
-        literal min(literal a, literal b) {
+        literal mk_min(literal a, literal b) {
             if (a == b) return a;
             m_stats.m_num_compiled_vars++;
-            return ctx.min(a, b);
+            return ctx.mk_min(a, b);
         }
 
         literal fresh() {
@@ -299,20 +299,20 @@ Notes:
             ctx.mk_clause(n, tmp.c_ptr());
         }
 
-        // y1 <= max(x1,x2)
-        // y2 <= min(x1,x2)
+        // y1 <= mk_max(x1,x2)
+        // y2 <= mk_min(x1,x2)
         void cmp_ge(literal x1, literal x2, literal y1, literal y2) {
-            add_clause(~y2, x1);
-            add_clause(~y2, x2);
-            add_clause(~y1, x1, x2);            
+            add_clause(ctx.mk_not(y2), x1);
+            add_clause(ctx.mk_not(y2), x2);
+            add_clause(ctx.mk_not(y1), x1, x2);            
         }
 
-        // max(x1,x2) <= y1
-        // min(x1,x2) <= y2
+        // mk_max(x1,x2) <= y1
+        // mk_min(x1,x2) <= y2
         void cmp_le(literal x1, literal x2, literal y1, literal y2) {
-            add_clause(~x1, y1);
-            add_clause(~x2, y1);
-            add_clause(~x1, ~x2, y2);
+            add_clause(ctx.mk_not(x1), y1);
+            add_clause(ctx.mk_not(x2), y1);
+            add_clause(ctx.mk_not(x1), ctx.mk_not(x2), y2);
         }
 
         void cmp_eq(literal x1, literal x2, literal y1, literal y2) {
@@ -376,8 +376,8 @@ Notes:
                    literal_vector& out) {
             TRACE("pb", tout << "merge a: " << a << " b: " << b << "\n";);
             if (a == 1 && b == 1) {
-                literal y1 = max(as[0], bs[0]);
-                literal y2 = min(as[0], bs[0]);
+                literal y1 = mk_max(as[0], bs[0]);
+                literal y2 = mk_min(as[0], bs[0]);
                 out.push_back(y1);
                 out.push_back(y2);
                 psort_nw<psort_expr>::cmp(as[0], bs[0], y1, y2);
@@ -453,8 +453,8 @@ Notes:
             out.push_back(as[0]);
             unsigned sz = std::min(as.size()-1, bs.size());
             for (unsigned i = 0; i < sz; ++i) {
-                literal y1 = max(as[i+1],bs[i]);
-                literal y2 = min(as[i+1],bs[i]);
+                literal y1 = mk_max(as[i+1],bs[i]);
+                literal y2 = mk_min(as[i+1],bs[i]);
                 psort_nw<psort_expr>::cmp(as[i+1], bs[i], y1, y2);
                 out.push_back(y1);
                 out.push_back(y2);
@@ -539,16 +539,16 @@ Notes:
                     literal_vector& out) {
             TRACE("pb", tout << "smerge: c:" << c << " a:" << a << " b:" << b << "\n";);
             if (a == 1 && b == 1 && c == 1) {
-                literal y = max(as[0], bs[0]);
+                literal y = mk_max(as[0], bs[0]);
                 if (m_t != GE) {
-                    // x1 <= max(x1,x2)
-                    // x2 <= max(x1,x2)
-                    add_clause(~as[0], y);
-                    add_clause(~bs[0], y);
+                    // x1 <= mk_max(x1,x2)
+                    // x2 <= mk_max(x1,x2)
+                    add_clause(ctx.mk_not(as[0]), y);
+                    add_clause(ctx.mk_not(bs[0]), y);
                 }
                 if (m_t != LE) {
-                    // max(x1,x2) <= x1, x2
-                    add_clause(~y, as[0], bs[0]);
+                    // mk_max(x1,x2) <= x1, x2
+                    add_clause(ctx.mk_not(y), as[0], bs[0]);
                 }
                 out.push_back(y);
             }
@@ -597,13 +597,13 @@ Notes:
                     literal z2 = out2.back();
                     out1.pop_back();
                     out2.pop_back();
-                    y = max(z1, z2);
+                    y = mk_max(z1, z2);
                     if (m_t != GE) {
-                        add_clause(~z1, y);
-                        add_clause(~z2, y);
+                        add_clause(ctx.mk_not(z1), y);
+                        add_clause(ctx.mk_not(z2), y);
                     }
                     if (m_t != LE) {
-                        add_clause(~y, z1, z2);
+                        add_clause(ctx.mk_not(y), z1, z2);
                     }
                 }
                 interleave(out1, out2, out);                 
@@ -664,31 +664,28 @@ Notes:
             }
             if (m_t != GE) {
                 for (unsigned i = 0; i < a; ++i) {
-                    add_clause(~as[i], out[i]);
+                    add_clause(ctx.mk_not(as[i]), out[i]);
                 }
                 for (unsigned i = 0; i < b; ++i) {
-                    add_clause(~bs[i], out[i]);
+                    add_clause(ctx.mk_not(bs[i]), out[i]);
                 }
                 for (unsigned i = 1; i <= a; ++i) {
                     for (unsigned j = 1; j <= b && i + j <= c; ++j) {
-                        add_clause(~as[i-1],~bs[j-1],out[i+j-1]);
+                        add_clause(ctx.mk_not(as[i-1]),ctx.mk_not(bs[j-1]),out[i+j-1]);
                     }
                 }
             }
             if (m_t != LE) {
-                for (unsigned k = 1; k <= c; ++k) {
-                    literal_vector ls;
-                    ls.push_back(~out[k-1]);
-                    if (k <= a) {
-                        ls.push_back(as[k-1]);
-                    }
-                    if (k <= b) {
-                        ls.push_back(bs[k-1]);
-                    }
-                    for (unsigned i = 1; i <= std::min(a,k-1); ++i) {
-                        if (k + 1 - i <= b) {
-                            ls.push_back(as[i-1]);
-                            ls.push_back(bs[k-i]);
+                literal_vector ls;
+                for (unsigned k = 0; k < c; ++k) {
+                    ls.reset();
+                    ls.push_back(ctx.mk_not(out[k]));
+                    for (unsigned i = 0; i < std::min(a,k + 1); ++i) {
+                        unsigned j = k - i;
+                        SASSERT(i + j == k);
+                        if (j < b) {
+                            ls.push_back(as[i]);
+                            ls.push_back(bs[j]);
                             add_clause(ls.size(), ls.c_ptr());
                             ls.pop_back();
                             ls.pop_back();
@@ -726,7 +723,7 @@ Notes:
             }
             if (m_t != LE) {                
                 for (unsigned k = 1; k <= m; ++k) {
-                    lits.push_back(~out[k-1]);
+                    lits.push_back(ctx.mk_not(out[k-1]));
                     add_subset(false, n-k+1, 0, lits, n, xs);
                     lits.pop_back();
                 }
@@ -754,7 +751,7 @@ Notes:
                 return;
             }
             for (unsigned i = offset; i < n - k + 1; ++i) {
-                lits.push_back(polarity?~xs[i]:xs[i]);
+                lits.push_back(polarity?ctx.mk_not(xs[i]):xs[i]);
                 add_subset(polarity, k-1, i+1, lits, n, xs);
                 lits.pop_back();
             }