From a880e5f49be687222b1dd26facf518a1fed7a5ec Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 24 Oct 2016 13:12:36 -0700
Subject: [PATCH 01/22] fix incorrection assertion when checking signs of
 literals, exposed by miTLS regressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 5f258fc61..832d4dac7 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3773,15 +3773,15 @@ namespace smt {
 #ifdef Z3DEBUG
             for (unsigned i = 0; i < num_lits; i++) {
                 literal l = lits[i];
-                if (m_manager.is_not(expr_lits.get(i))) {
+                if (expr_signs[i] != l.sign()) {
+                    expr* real_atom;
+                    VERIFY(m_manager.is_not(expr_lits.get(i), real_atom));
                     // the sign must have flipped when internalizing
-                    expr * real_atom = to_app(expr_lits.get(i))->get_arg(0);
+                    CTRACE("resolve_conflict_bug", real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m_manager) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";);
                     SASSERT(real_atom == bool_var2expr(l.var()));
-                    SASSERT(expr_signs[i]    != l.sign());
                 }
                 else {
                     SASSERT(expr_lits.get(i) == bool_var2expr(l.var()));
-                    SASSERT(expr_signs[i]    == l.sign());
                 }
             }
 #endif

From e4d2c5867aa24c04c87c48bb2bec453f401f66e6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 24 Oct 2016 15:52:47 -0700
Subject: [PATCH 02/22] remove dead (and incorrect) code

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_solver.cpp |  22 +++++---
 src/solver/mus.cpp     | 115 ++++-------------------------------------
 2 files changed, 26 insertions(+), 111 deletions(-)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 1e667eccc..c3aaa5697 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3151,7 +3151,7 @@ namespace sat {
 
     lbool solver::get_consequences(literal_vector const& asms, literal_vector const& lits, vector<literal_vector>& conseq) {
         m_antecedents.reset();
-        literal_set unfixed(lits), assumptions(asms);
+        literal_set vars(lits), assumptions(asms);
 
         pop_to_base_level();
         if (inconsistent()) return l_false;
@@ -3162,11 +3162,12 @@ namespace sat {
         propagate(false);
         if (check_inconsistent()) return l_false;
        
-        unsigned num_units = 0;
-        extract_fixed_consequences(num_units, assumptions, unfixed, conseq);
-        while (!unfixed.empty()) {
+        unsigned num_units = 0, num_iterations = 0;
+        extract_fixed_consequences(num_units, assumptions, vars, conseq);
+        while (!vars.empty()) {
+            ++num_iterations;
             checkpoint();
-            literal_set::iterator it = unfixed.begin(), end = unfixed.end();
+            literal_set::iterator it = vars.begin(), end = vars.end();
             for (; it != end; ++it) {
                 literal lit = *it;
                 if (value(lit) != l_undef) {
@@ -3197,9 +3198,16 @@ namespace sat {
                 m_inconsistent = false;
             }
             if (is_sat == l_true) {
-                delete_unfixed(unfixed);
+                delete_unfixed(vars);
             }
-            extract_fixed_consequences(num_units, assumptions, unfixed, conseq);            
+            extract_fixed_consequences(num_units, assumptions, vars, conseq);            
+            IF_VERBOSE(1, verbose_stream() << "(get-consequences"
+                       << " iterations: " << num_iterations
+                       << " variables: " << vars.size()
+                       << " fixed: " << conseq.size()
+                       << " unfixed: " << lits.size() - conseq.size() - vars.size()
+                       << ")\n";);
+
         }
         return l_true;
     }
diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp
index 81635f906..91d47386e 100644
--- a/src/solver/mus.cpp
+++ b/src/solver/mus.cpp
@@ -239,6 +239,17 @@ struct mus::imp {
         return l_false;
     }
 
+    void get_core(expr_set& core) {
+        core.reset();
+        ptr_vector<expr> core_exprs;
+        m_solver.get_unsat_core(core_exprs);
+        for (unsigned i = 0; i < core_exprs.size(); ++i) {
+            if (m_expr2lit.contains(core_exprs[i])) {
+                core.insert(core_exprs[i]);
+            }
+        }
+    }
+
     bool have_intersection(expr_set const& A, expr_set const& B) {
         if (A.size() < B.size()) {
             expr_set::iterator it = A.begin(), end = A.end();
@@ -345,110 +356,6 @@ struct mus::imp {
         return m_weight;
     }
 
-
-    lbool qx(expr_ref_vector& mus) {
-        expr_set core, support;
-        for (unsigned i = 0; i < m_lit2expr.size(); ++i) {
-            core.insert(m_lit2expr[i].get());
-        }
-        lbool is_sat = qx(core, support, false);
-        if (is_sat == l_true) {
-            expr_set::iterator it = core.begin(), end = core.end();
-            mus.reset();
-            for (; it != end; ++it) {
-                mus.push_back(*it);
-            }
-        }
-        return is_sat;
-    }
-
-    lbool qx(expr_set& assignment, expr_set& support, bool has_support) {
-        lbool is_sat = l_true;
-#if 0
-        if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
-            IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
-            return l_true;
-        }
-#endif
-        if (has_support) {
-            expr_ref_vector asms(m);
-            scoped_append _sa1(*this, asms, support);
-            scoped_append _sa2(*this, asms, m_assumptions);
-            is_sat = m_solver.check_sat(asms);
-            switch (is_sat) {
-            case l_false: {
-                expr_set core; 
-                get_core(core);
-                support &= core;
-                assignment.reset();
-                return l_true;
-            }
-            case l_undef:
-                return l_undef;
-            case l_true:
-                update_model();
-                break;
-            default:
-                break;
-            }
-        }
-        if (assignment.size() == 1) {
-            return l_true;
-        }
-        expr_set assign2;
-        split(assignment, assign2);
-        support |= assignment;
-        is_sat = qx(assign2, support, !assignment.empty());        
-        unsplit(support, assignment);
-        if (is_sat != l_true) return is_sat;
-        support |= assign2;
-        is_sat = qx(assignment, support, !assign2.empty());
-        assignment |= assign2;
-        unsplit(support, assign2);
-        return is_sat;
-    }
-
-    void get_core(expr_set& core) {
-        core.reset();
-        ptr_vector<expr> core_exprs;
-        m_solver.get_unsat_core(core_exprs);
-        for (unsigned i = 0; i < core_exprs.size(); ++i) {
-            if (m_expr2lit.contains(core_exprs[i])) {
-                core.insert(core_exprs[i]);
-            }
-        }
-    }
-
-    void unsplit(expr_set& A, expr_set& B) {
-        expr_set A1, B1;
-        expr_set::iterator it = A.begin(), end = A.end();
-        for (; it != end; ++it) {
-            if (B.contains(*it)) {
-                B1.insert(*it);
-            }
-            else {
-                A1.insert(*it);
-            }
-        }
-        A = A1;
-        B = B1;
-    }
-
-    void split(expr_set& lits1, expr_set& lits2) {
-        unsigned half = lits1.size()/2;
-        expr_set lits3;
-        expr_set::iterator it = lits1.begin(), end = lits1.end();
-        for (unsigned i = 0; it != end; ++it, ++i) {
-            if (i < half) {
-                lits3.insert(*it);
-            }
-            else {
-                lits2.insert(*it);
-            }
-        }
-        lits1 = lits3;
-    }
-
 };
 
 mus::mus(solver& s) {

From b82b53dc349cf90b522983d3d03afec1d1a85167 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 24 Oct 2016 17:41:52 -0700
Subject: [PATCH 03/22] add handling of pseudo-boolean inequalities that use
 if-expressions over Booleans and arihmetic instead of built-in PB predicates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/arith_decl_plugin.h             |   4 +
 src/ast/rewriter/pb2bv_rewriter.cpp     | 162 ++++++++++++++++++------
 src/tactic/portfolio/enum2bv_solver.cpp |   2 -
 3 files changed, 125 insertions(+), 43 deletions(-)

diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 4f0379674..410c50852 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -264,6 +264,10 @@ public:
     bool is_ge(expr const * n) const { return is_app_of(n, m_afid, OP_GE); }
     bool is_lt(expr const * n) const { return is_app_of(n, m_afid, OP_LT); }
     bool is_gt(expr const * n) const { return is_app_of(n, m_afid, OP_GT); }
+    bool is_le(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LE); }
+    bool is_ge(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GE); }
+    bool is_lt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LT); }
+    bool is_gt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GT); }
     bool is_add(expr const * n) const { return is_app_of(n, m_afid, OP_ADD); }
     bool is_sub(expr const * n) const { return is_app_of(n, m_afid, OP_SUB); }
     bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); }
diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 48d566f11..5cd7789ff 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -79,6 +79,9 @@ struct pb2bv_rewriter::imp {
         pb_util      pb;
         bv_util      bv;
         expr_ref_vector m_trail;
+        expr_ref_vector m_args;
+        rational     m_k;
+        vector<rational> m_coeffs;
 
         template<lbool is_le>
         expr_ref mk_le_ge(expr_ref_vector& fmls, expr* a, expr* b, expr* bound) {
@@ -109,8 +112,22 @@ struct pb2bv_rewriter::imp {
         // The procedure for checking >= k is symmetric and checking for = k is
         // achieved by checking <= k on intermediary addends and the resulting sum is = k.
         // 
+        // is_le = l_true  -  <=
+        // is_le = l_undef -  =
+        // is_le = l_false -  >= 
+        //
         template<lbool is_le>
-        expr_ref mk_le_ge(func_decl *f, unsigned sz, expr * const* args, rational const & k) {
+        expr_ref mk_le_ge(unsigned sz, expr * const* args, rational const & k) {
+            TRACE("pb", 
+                  for (unsigned i = 0; i < sz; ++i) {
+                      tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " ";
+                  }
+                  switch (is_le) {
+                  case l_true: tout << "<= "; break;
+                  case l_undef: tout << "= "; break;
+                  case l_false: tout << ">= "; break;
+                  }
+                  tout << m_k << "\n";);
             if (k.is_zero()) {
                 if (is_le != l_false) {
                     return expr_ref(m.mk_not(mk_or(m, sz, args)), m);
@@ -119,6 +136,9 @@ struct pb2bv_rewriter::imp {
                     return expr_ref(m.mk_true(), m);
                 }
             }
+            if (k.is_neg()) {
+                return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m);
+            }
             SASSERT(k.is_pos());
             expr_ref zero(m), bound(m);
             expr_ref_vector es(m), fmls(m);
@@ -126,7 +146,8 @@ struct pb2bv_rewriter::imp {
             zero = bv.mk_numeral(rational(0), nb);
             bound = bv.mk_numeral(k, nb);
             for (unsigned i = 0; i < sz; ++i) {
-                if (pb.get_coeff(f, i) > k) {
+                SASSERT(!m_coeffs[i].is_neg());
+                if (m_coeffs[i] > k) {
                     if (is_le != l_false) {
                         fmls.push_back(m.mk_not(args[i]));
                     }
@@ -135,7 +156,7 @@ struct pb2bv_rewriter::imp {
                     }
                 }
                 else {
-                    es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), nb), zero));
+                    es.push_back(mk_ite(args[i], bv.mk_numeral(m_coeffs[i], nb), zero));
                 }
             }
             while (es.size() > 1) {
@@ -165,6 +186,10 @@ struct pb2bv_rewriter::imp {
         expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) {
             decl_kind kind = f->get_decl_kind();
             rational k = pb.get_k(f);
+            m_coeffs.reset();
+            for (unsigned i = 0; i < sz; ++i) {
+                m_coeffs.push_back(pb.get_coeff(f, i));
+            }
             SASSERT(!k.is_neg());
             switch (kind) {
             case OP_PB_GE:
@@ -173,13 +198,13 @@ struct pb2bv_rewriter::imp {
                 nargs.append(sz, args);
                 dualize(f, nargs, k);
                 SASSERT(!k.is_neg());
-                return mk_le_ge<l_true>(f, sz, nargs.c_ptr(), k);
+                return mk_le_ge<l_true>(sz, nargs.c_ptr(), k);
             }
             case OP_PB_LE:
             case OP_AT_MOST_K:
-                return mk_le_ge<l_true>(f, sz, args, k);
+                return mk_le_ge<l_true>(sz, args, k);
             case OP_PB_EQ:
-                return mk_le_ge<l_undef>(f, sz, args, k);
+                return mk_le_ge<l_undef>(sz, args, k);
             default:
                 UNREACHABLE();
                 return expr_ref(m.mk_true(), m);
@@ -228,7 +253,6 @@ struct pb2bv_rewriter::imp {
             }
         }
 
-
     public:
 
         card2bv_rewriter(imp& i, ast_manager& m):
@@ -238,7 +262,8 @@ struct pb2bv_rewriter::imp {
             pb(m),
             bv(m),
             m_sort(*this),
-            m_trail(m)
+            m_trail(m),
+            m_args(m)
         {}
 
         br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
@@ -247,8 +272,31 @@ struct pb2bv_rewriter::imp {
                 ++m_imp.m_num_translated;
                 return BR_DONE;
             }
-            else if (f->get_family_id() == au.get_family_id() && mk_arith(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);
                 return BR_DONE;
             }
             else {
@@ -256,43 +304,75 @@ struct pb2bv_rewriter::imp {
             }
         }
 
-        //
-        // NSB: review
-        // we should remove this code and rely on a layer above to deal with 
-        // whatever it accomplishes. It seems to break types.
-        // 
-        bool mk_arith(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
-            if (f->get_decl_kind() == OP_ADD) {
-                unsigned bits = 0;
-                for (unsigned i = 0; i < sz; i++) {
-                    rational val1, val2;
-                    if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) {
-                        bits += val1.get_num_bits();
+        bool is_pb(expr* x, expr* y) {
+            m_args.reset();
+            m_coeffs.reset();
+            m_k.reset();
+            return is_pb(x, rational::one()) && is_pb(y, rational::minus_one());
+        }
+
+        bool is_pb(expr* e, rational const& mul) {
+            if (!is_app(e)) {
+                return false;
+            }
+            app* a = to_app(e);
+            rational r, r1, r2;
+            expr* c, *th, *el;
+            unsigned sz = a->get_num_args();
+            if (a->get_family_id() == au.get_family_id()) {
+                switch (a->get_decl_kind()) {
+                case OP_ADD:
+                    for (unsigned i = 0; i < sz; ++i) {
+                        if (!is_pb(a->get_arg(i), mul)) return false;
                     }
-                    else if (m.is_ite(args[i]) &&
-                             au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() &&
-                             au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) {
-                        bits++;                        
+                    return true;
+                case OP_SUB: {
+                    if (!is_pb(a->get_arg(0), mul)) return false;
+                    r = -mul;
+                    for (unsigned i = 1; i < sz; ++i) {
+                        if (!is_pb(a->get_arg(1), r)) return false;
                     }
-                    else
-                        return false;
+                    return true;
+                }
+                case OP_UMINUS:
+                    return is_pb(a->get_arg(0), -mul);
+                case OP_NUM:
+                    VERIFY(au.is_numeral(a, r));
+                    m_k += mul * r;
+                    return true;
+                case OP_MUL:
+                    if (sz != 2) {
+                        return false;
+                    }
+                    if (au.is_numeral(a->get_arg(0), r)) {
+                        r *= mul;
+                        return is_pb(a->get_arg(1), r);
+                    }
+                    if (au.is_numeral(a->get_arg(1), r)) {
+                        r *= mul;
+                        return is_pb(a->get_arg(0), r);
+                    }
+                    return false;
+                default:
+                    return false;
+                }
+            }
+            if (m.is_ite(a, c, th, el) && au.is_numeral(th, r1) && au.is_numeral(el, r2)) {
+                r1 *= mul;
+                r2 *= mul;
+                if (r1 < r2) {
+                    m_args.push_back(::mk_not(m, c));
+                    m_coeffs.push_back(r2-r1);
+                    m_k -= r1;
+                }
+                else {
+                    m_args.push_back(c);
+                    m_coeffs.push_back(r1-r2);
+                    m_k -= r2;
                 }
-                
-                result = 0;
-                for (unsigned i = 0; i < sz; i++) {
-                    rational val1, val2;
-                    expr * q;
-                    if (au.is_int(args[i]) && au.is_numeral(args[i], val1))
-                        q = bv.mk_numeral(val1, bits);
-                    else
-                        q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits));
-                    result = (i == 0) ? q : bv.mk_bv_add(result.get(), q);
-                }                
                 return true;
             }
-            else {
-                return false;
-            } 
+            return false;
         }
 
         void mk_pb(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index 369402114..b0f11cb91 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -115,8 +115,6 @@ public:
             }
         }
         lbool r = m_solver->get_consequences(asms, bvars, consequences);
-        std::cout << consequences.size() << "\n";
-
 
         // translate bit-vector consequences back to enumeration types
         for (unsigned i = 0; i < consequences.size(); ++i) {

From fefd00aa4980dd7410f2315a6e3033c349f6b266 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 24 Oct 2016 20:28:56 -0700
Subject: [PATCH 04/22] fix sign of constant in pb constraint

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/pb2bv_rewriter.cpp | 36 ++---------------------------
 1 file changed, 2 insertions(+), 34 deletions(-)

diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 5cd7789ff..4f538867e 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -29,39 +29,6 @@ Notes:
 
 struct pb2bv_rewriter::imp {
 
-    struct argc_t {
-        expr*    m_arg;
-        rational m_coeff;
-        argc_t():m_arg(0), m_coeff(0) {}
-        argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {}
-    };
-    
-    struct argc_gt {
-        bool operator()(argc_t const& a, argc_t const& b) const {
-            return a.m_coeff > b.m_coeff;
-        }
-    };
-
-    struct argc_entry {
-        unsigned m_index;
-        rational m_k;
-        expr*    m_value;
-        argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {}
-        argc_entry():m_index(0), m_k(0), m_value(0) {}
-        
-        struct eq {
-            bool operator()(argc_entry const& a, argc_entry const& b) const {
-                return a.m_index == b.m_index && a.m_k == b.m_k;
-            }
-        };
-        struct hash {
-            unsigned operator()(argc_entry const& a) const {
-                return a.m_index ^ a.m_k.hash();
-            }
-        };
-    };
-    typedef hashtable<argc_entry, argc_entry::hash, argc_entry::eq> argc_cache;
-
     ast_manager&              m;
     params_ref                m_params;
     expr_ref_vector           m_lemmas;
@@ -121,6 +88,7 @@ struct pb2bv_rewriter::imp {
             TRACE("pb", 
                   for (unsigned i = 0; i < sz; ++i) {
                       tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " ";
+                      if (i + 1 < sz && !m_coeffs[i+1].is_neg()) tout << "+ ";
                   }
                   switch (is_le) {
                   case l_true: tout << "<= "; break;
@@ -338,7 +306,7 @@ struct pb2bv_rewriter::imp {
                     return is_pb(a->get_arg(0), -mul);
                 case OP_NUM:
                     VERIFY(au.is_numeral(a, r));
-                    m_k += mul * r;
+                    m_k -= mul * r;
                     return true;
                 case OP_MUL:
                     if (sz != 2) {

From 6ea45b4d65f36f0299007dc172477ec6e8478727 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 25 Oct 2016 14:23:55 +0100
Subject: [PATCH 05/22] fix for Python API installation

---
 scripts/mk_util.py | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 309b08297..a86499149 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1505,6 +1505,9 @@ class PythonInstallComponent(Component):
                                            os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'),
                                            in_prefix=self.in_prefix_install
                                           )
+        MakeRuleCmd.remove_installed_files(out,
+                                           os.path.join(self.pythonPkgDir, 'z3', 'lib',
+                                                        self.libz3Component.dll_file()))
 
     def mk_makefile(self, out):
         return

From 8c5c564d6ce49c1bfc80175a457712ee30691af7 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 25 Oct 2016 14:31:29 +0100
Subject: [PATCH 06/22] fixed initialization order warning in pb2bv_rewriter

---
 src/ast/rewriter/pb2bv_rewriter.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 4f538867e..8871c3dd8 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -224,12 +224,12 @@ struct pb2bv_rewriter::imp {
     public:
 
         card2bv_rewriter(imp& i, ast_manager& m):
+            m_sort(*this),
             m(m),
             m_imp(i),
             au(m),
             pb(m),
             bv(m),
-            m_sort(*this),
             m_trail(m),
             m_args(m)
         {}

From c7fddf80c2a84d5235ddf4325cd2194de66d0083 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 25 Oct 2016 14:34:00 +0100
Subject: [PATCH 07/22] fixed unhandled case warning in test/qe_arith.cpp

---
 src/test/qe_arith.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index 79495e24f..a73f7ed38 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -375,6 +375,9 @@ static void add_random_ineq(
     case opt::t_le:
         fml = a.mk_le(t1, t2);
         break;
+    case opt::t_mod:
+        NOT_IMPLEMENTED_YET();        
+        break;        
     }
     fmls.push_back(fml);
     mbo.add_constraint(vars, rational(coeff), rel);

From 461e88e34cfd6819343297e1ee87543a1ea3817e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 25 Oct 2016 20:32:13 -0700
Subject: [PATCH 08/22] additional robustness check for incremental sat solver
 core when it recieves interpreted constants, added PB equality to interface
 and special handling of equalities to adddress performance gap documented in
 #755

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 contrib/cmake/src/solver/CMakeLists.txt       |   1 +
 src/api/api_pb.cpp                            |  18 ++
 src/api/dotnet/Context.cs                     |  15 ++
 src/api/dotnet/Optimize.cs                    |   9 +-
 src/api/python/z3/z3.py                       |  20 ++
 src/api/z3_api.h                              |  16 ++
 src/sat/sat_solver/inc_sat_solver.cpp         |  10 +
 src/sat/tactic/goal2sat.cpp                   |  17 +-
 src/sat/tactic/goal2sat.h                     |   6 +-
 src/smt/tactic/smt_tactic.cpp                 |  55 +-----
 src/smt/tactic/smt_tactic.h                   |   2 -
 src/solver/combined_solver.cpp                |   1 +
 src/solver/solver2tactic.cpp                  | 179 ++++++++++++++++++
 src/solver/solver2tactic.h                    |  30 +++
 src/solver/tactic2solver.cpp                  |   1 +
 src/tactic/arith/bound_manager.cpp            |  39 +++-
 src/tactic/arith/bound_manager.h              |   2 +
 src/tactic/nlsat_smt/nl_purify_tactic.cpp     |   1 +
 .../portfolio/bounded_int2bv_solver.cpp       |  10 +
 src/tactic/portfolio/smt_strategic_solver.cpp |   3 +
 src/util/sorting_network.h                    |  79 ++++++--
 21 files changed, 430 insertions(+), 84 deletions(-)
 create mode 100644 src/solver/solver2tactic.cpp
 create mode 100644 src/solver/solver2tactic.h

diff --git a/contrib/cmake/src/solver/CMakeLists.txt b/contrib/cmake/src/solver/CMakeLists.txt
index 8142ca872..7f54e7745 100644
--- a/contrib/cmake/src/solver/CMakeLists.txt
+++ b/contrib/cmake/src/solver/CMakeLists.txt
@@ -5,6 +5,7 @@ z3_add_component(solver
     mus.cpp
     solver.cpp
     solver_na2as.cpp
+    solver2tactic.cpp
     tactic2solver.cpp
   COMPONENT_DEPENDENCIES
     model
diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp
index 6d5a56d2c..b7c28c34f 100644
--- a/src/api/api_pb.cpp
+++ b/src/api/api_pb.cpp
@@ -57,5 +57,23 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, 
+                             Z3_ast const args[], int _coeffs[],
+                             int k) {
+        Z3_TRY;
+        LOG_Z3_mk_pble(c, num_args, args, _coeffs, k);
+        RESET_ERROR_CODE();
+        pb_util util(mk_c(c)->m());
+        vector<rational> coeffs;
+        for (unsigned i = 0; i < num_args; ++i) {
+            coeffs.push_back(rational(_coeffs[i]));
+        }
+        ast* a = util.mk_eq(num_args, coeffs.c_ptr(), to_exprs(args), rational(k));
+        mk_c(c)->save_ast_trail(a);
+        check_sorts(c, a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(0);
+    }
+
 
 };
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 6ca48fcb0..c3c33a41e 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2640,6 +2640,21 @@ namespace Microsoft.Z3
                                                           AST.ArrayToNative(args),
                                                           coeffs, k));
         }
+
+        /// <summary>
+        /// Create a pseudo-Boolean equal constraint.
+        /// </summary>
+        public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
+        {
+           Contract.Requires(args != null);
+           Contract.Requires(coeffs != null);
+           Contract.Requires(args.Length == coeffs.Length);
+           Contract.Requires(Contract.Result<BoolExpr[]>() != null);
+           CheckContextMatch<BoolExpr>(args);
+           return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length,
+                                                          AST.ArrayToNative(args),
+                                                          coeffs, k));
+        }
         #endregion
 
         #region Numerals
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 036aaf2f2..c8954a473 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -258,10 +258,13 @@ namespace Microsoft.Z3
 	/// <summary>
 	/// Return a string the describes why the last to check returned unknown
 	/// </summary>	
-    	public String getReasonUnknown()
+    	public String ReasonUnknown
     	{
-            Contract.Ensures(Contract.Result<string>() != null);
-            return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
+            get 
+            {
+                Contract.Ensures(Contract.Result<string>() != null);
+                return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
+            }
     	}
 
 
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index a037bbc5d..514a45fc6 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -7654,6 +7654,26 @@ def PbLe(args, k):
         _coeffs[i] = coeffs[i]
     return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
+def PbEq(args, k):
+    """Create a Pseudo-Boolean inequality k constraint.
+
+    >>> a, b, c = Bools('a b c')
+    >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
+    """
+    args  = _get_args(args)
+    args, coeffs = zip(*args)
+    if __debug__:
+        _z3_assert(len(args) > 0, "Non empty list of arguments expected")
+    ctx   = _ctx_from_ast_arg_list(args)
+    if __debug__:
+        _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
+    args = _coerce_expr_list(args, ctx)
+    _args, sz = _to_ast_array(args)
+    _coeffs = (ctypes.c_int * len(coeffs))()
+    for i in range(len(coeffs)):
+        _coeffs[i] = coeffs[i]
+    return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
+
 
 def solve(*args, **keywords):
     """Solve the constraints `*args`.
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 9e9771884..069f83340 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -861,6 +861,9 @@ typedef enum
       - Z3_OP_PB_GE: Generalized Pseudo-Boolean cardinality constraint.
               Example  2*x + 3*y + 2*z >= 4
 
+      - Z3_OP_PB_EQ: Generalized Pseudo-Boolean equality constraint.
+              Example  2*x + 1*y + 2*z + 1*u = 4
+
       - Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: Floating-point rounding mode RNE
 
       - Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: Floating-point rounding mode RNA
@@ -1166,6 +1169,7 @@ typedef enum {
     Z3_OP_PB_AT_MOST=0x900,
     Z3_OP_PB_LE,
     Z3_OP_PB_GE,
+    Z3_OP_PB_EQ,
 
     // Floating-Point Arithmetic
     Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
@@ -3913,6 +3917,18 @@ extern "C" {
                              Z3_ast const args[], int coeffs[],
                              int k);
 
+    /**
+       \brief Pseudo-Boolean relations.
+
+       Encode k1*p1 + k2*p2 + ... + kn*pn = k
+
+       def_API('Z3_mk_pbeq', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
+    */
+
+    Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
+                             Z3_ast const args[], int coeffs[],
+                             int k);
+
     /**
        \brief Convert a \c Z3_func_decl into \c Z3_ast. This is just type casting.
 
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 349b60f55..d091339bd 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -371,8 +371,18 @@ private:
             return l_undef;
         }
         g = m_subgoals[0];
+        expr_ref_vector atoms(m);
         TRACE("sat", g->display_with_dependencies(tout););
         m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
+        m_goal2sat.get_interpreted_atoms(atoms);
+        if (!atoms.empty()) {
+            std::stringstream strm;
+            strm << "interpreted atoms sent to SAT solver " << atoms;
+            TRACE("sat", std::cout << strm.str() << "\n";);
+            IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
+            set_reason_unknown(strm.str().c_str());
+            return l_undef;
+        }
         return l_true;
     }
 
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 4d5542866..136921914 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -59,6 +59,7 @@ struct goal2sat::imp {
     bool                        m_ite_extra;
     unsigned long long          m_max_memory;
     expr_ref_vector             m_trail;
+    expr_ref_vector             m_interpreted_atoms;
     bool                        m_default_external;
     
     imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
@@ -67,6 +68,7 @@ struct goal2sat::imp {
         m_map(map),
         m_dep2asm(dep2asm),
         m_trail(m),
+        m_interpreted_atoms(m),
         m_default_external(default_external) {
         updt_params(p);
         m_true = sat::null_bool_var;
@@ -128,6 +130,9 @@ struct goal2sat::imp {
                 m_map.insert(t, v);
                 l = sat::literal(v, sign);
                 TRACE("goal2sat", tout << "new_var: " << v << "\n" << mk_ismt2_pp(t, m) << "\n";);
+                if (ext && !is_uninterp_const(t)) {
+                    m_interpreted_atoms.push_back(t);
+                }
             }
         }
         else {
@@ -474,7 +479,7 @@ bool goal2sat::has_unsupported_bool(goal const & g) {
     return test<unsupported_bool_proc>(g);
 }
 
-goal2sat::goal2sat():m_imp(0) {
+goal2sat::goal2sat():m_imp(0), m_interpreted_atoms(0) {
 }
 
 void goal2sat::collect_param_descrs(param_descrs & r) {
@@ -492,10 +497,20 @@ struct goal2sat::scoped_set_imp {
     }
 };
 
+
 void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) {
     imp proc(g.m(), p, t, m, dep2asm, default_external);
     scoped_set_imp set(this, &proc);
     proc(g);
+    dealloc(m_interpreted_atoms);
+    m_interpreted_atoms = alloc(expr_ref_vector, g.m());
+    m_interpreted_atoms->append(proc.m_interpreted_atoms);
+}
+
+void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) {
+    if (m_interpreted_atoms) {
+        atoms.append(*m_interpreted_atoms);
+    }
 }
 
 
diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
index c6776f2f7..cd63cd497 100644
--- a/src/sat/tactic/goal2sat.h
+++ b/src/sat/tactic/goal2sat.h
@@ -38,8 +38,11 @@ class goal2sat {
     struct imp;
     imp *  m_imp;
     struct scoped_set_imp;
+    expr_ref_vector* m_interpreted_atoms;
+
 public:
     goal2sat();
+    ~goal2sat() { dealloc(m_interpreted_atoms); }
 
     typedef obj_map<expr, sat::literal> dep2asm_map;
 
@@ -53,12 +56,13 @@ public:
        
        \remark m doesn't need to be empty. the definitions there are 
        reused.
-    
+       
        \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
        an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory).
     */
     void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
 
+    void get_interpreted_atoms(expr_ref_vector& atoms);
 
 };
 
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index f2fbcf6d9..2909d8848 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -24,63 +24,10 @@ Notes:
 #include"rewriter_types.h"
 #include"filter_model_converter.h"
 #include"ast_util.h"
+#include"solver2tactic.h"
 
 typedef obj_map<expr, expr *> expr2expr_map;
 
-void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, expr2expr_map& bool2dep, ref<filter_model_converter>& fmc) {
-    expr2expr_map dep2bool;
-    ptr_vector<expr> deps;
-    ast_manager& m = g->m();
-    expr_ref_vector clause(m);
-    unsigned sz = g->size();
-    for (unsigned i = 0; i < sz; i++) {
-        expr * f            = g->form(i);
-        expr_dependency * d = g->dep(i);
-        if (d == 0 || !g->unsat_core_enabled()) {
-            clauses.push_back(f);
-        }
-        else {
-            // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
-            clause.reset();
-            clause.push_back(f);
-            deps.reset();
-            m.linearize(d, deps);
-            SASSERT(!deps.empty()); // d != 0, then deps must not be empty
-            ptr_vector<expr>::iterator it  = deps.begin();
-            ptr_vector<expr>::iterator end = deps.end();
-            for (; it != end; ++it) {
-                expr * d = *it;
-                if (is_uninterp_const(d) && m.is_bool(d)) {
-                    // no need to create a fresh boolean variable for d
-                    if (!bool2dep.contains(d)) {
-                        assumptions.push_back(d);
-                        bool2dep.insert(d, d);
-                    }
-                    clause.push_back(m.mk_not(d));
-                }
-                else {
-                    // must normalize assumption
-                    expr * b = 0;
-                    if (!dep2bool.find(d, b)) {
-                        b = m.mk_fresh_const(0, m.mk_bool_sort());
-                        dep2bool.insert(d, b);
-                        bool2dep.insert(b, d);
-                        assumptions.push_back(b);
-                        if (!fmc) {
-                            fmc = alloc(filter_model_converter, m);
-                        }
-                        fmc->insert(to_app(b)->get_decl());
-                    }
-                    clause.push_back(m.mk_not(b));
-                }
-            }
-            SASSERT(clause.size() > 1);
-            expr_ref cls(m);
-            cls = mk_or(m, clause.size(), clause.c_ptr());
-            clauses.push_back(cls);
-        }
-    }
-}
 
 class smt_tactic : public tactic {
     smt_params                   m_params;
diff --git a/src/smt/tactic/smt_tactic.h b/src/smt/tactic/smt_tactic.h
index dd113634b..a23695fd1 100644
--- a/src/smt/tactic/smt_tactic.h
+++ b/src/smt/tactic/smt_tactic.h
@@ -32,8 +32,6 @@ tactic * mk_smt_tactic(params_ref const & p = params_ref());
 tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref());
 
 
-void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, obj_map<expr, expr*>& bool2dep, ref<filter_model_converter>& fmc);
-
 /*
   ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)") 
 */
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index fc76f85c1..2856315bd 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -196,6 +196,7 @@ public:
 
     virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
         switch_inc_mode();
+        m_use_solver1_results = false;
         return m_solver2->get_consequences(asms, vars, consequences);
     }
 
diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
new file mode 100644
index 000000000..53b120fea
--- /dev/null
+++ b/src/solver/solver2tactic.cpp
@@ -0,0 +1,179 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    solver2tactic.cpp
+
+Abstract:
+
+    Convert solver to a tactic.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-10-17
+
+Notes:
+   
+--*/
+
+#include "solver.h"
+#include "tactic.h"
+#include"filter_model_converter.h"
+#include "solver2tactic.h"
+#include "ast_util.h"
+
+typedef obj_map<expr, expr *> expr2expr_map;
+
+void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, expr2expr_map& bool2dep, ref<filter_model_converter>& fmc) {
+    expr2expr_map dep2bool;
+    ptr_vector<expr> deps;
+    ast_manager& m = g->m();
+    expr_ref_vector clause(m);
+    unsigned sz = g->size();
+    for (unsigned i = 0; i < sz; i++) {
+        expr * f            = g->form(i);
+        expr_dependency * d = g->dep(i);
+        if (d == 0 || !g->unsat_core_enabled()) {
+            clauses.push_back(f);
+        }
+        else {
+            // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
+            clause.reset();
+            clause.push_back(f);
+            deps.reset();
+            m.linearize(d, deps);
+            SASSERT(!deps.empty()); // d != 0, then deps must not be empty
+            ptr_vector<expr>::iterator it  = deps.begin();
+            ptr_vector<expr>::iterator end = deps.end();
+            for (; it != end; ++it) {
+                expr * d = *it;
+                if (is_uninterp_const(d) && m.is_bool(d)) {
+                    // no need to create a fresh boolean variable for d
+                    if (!bool2dep.contains(d)) {
+                        assumptions.push_back(d);
+                        bool2dep.insert(d, d);
+                    }
+                    clause.push_back(m.mk_not(d));
+                }
+                else {
+                    // must normalize assumption
+                    expr * b = 0;
+                    if (!dep2bool.find(d, b)) {
+                        b = m.mk_fresh_const(0, m.mk_bool_sort());
+                        dep2bool.insert(d, b);
+                        bool2dep.insert(b, d);
+                        assumptions.push_back(b);
+                        if (!fmc) {
+                            fmc = alloc(filter_model_converter, m);
+                        }
+                        fmc->insert(to_app(b)->get_decl());
+                    }
+                    clause.push_back(m.mk_not(b));
+                }
+            }
+            SASSERT(clause.size() > 1);
+            expr_ref cls(m);
+            cls = mk_or(m, clause.size(), clause.c_ptr());
+            clauses.push_back(cls);
+        }
+    }
+}
+
+class solver2tactic : public tactic {
+    ast_manager& m;
+    ref<solver> m_solver;
+    params_ref m_params;
+
+public:
+    solver2tactic(solver* s):
+        m(s->get_manager()),
+        m_solver(s)
+    {}
+    
+    virtual void updt_params(params_ref const & p) {
+        m_solver->updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        m_solver->collect_param_descrs(r);
+    }
+
+    virtual void operator()(/* in */  goal_ref const & in, 
+                            /* out */ goal_ref_buffer & result, 
+                            /* out */ model_converter_ref & mc, 
+                            /* out */ proof_converter_ref & pc,
+                            /* out */ expr_dependency_ref & core) {
+        expr_ref_vector clauses(m);
+        expr2expr_map               bool2dep;
+        ptr_vector<expr>            assumptions;
+        ref<filter_model_converter> fmc;
+        extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc);
+        m_solver->push();
+        m_solver->assert_expr(clauses);
+        lbool r = m_solver->check_sat(assumptions.size(), assumptions.c_ptr()); 
+        switch (r) {
+        case l_true: 
+            if (in->models_enabled()) {
+                model_ref mdl;
+                m_solver->get_model(mdl);
+                mc = model2model_converter(mdl.get());
+                mc = concat(fmc.get(), mc.get());
+            }
+            in->reset();
+            result.push_back(in.get());
+            pc = 0;
+            core = 0;
+            break;
+        case l_false: {
+            in->reset();
+            proof* pr = 0;
+            expr_dependency* lcore = 0;
+            if (in->proofs_enabled()) {
+                pr = m_solver->get_proof();
+            }
+            if (in->unsat_core_enabled()) {
+                ptr_vector<expr> core;
+                m_solver->get_unsat_core(core);
+                for (unsigned i = 0; i < core.size(); ++i) {
+                    lcore = m.mk_join(lcore, m.mk_leaf(bool2dep.find(core[i])));
+                }
+            }
+            in->assert_expr(m.mk_false(), pr, lcore);
+            result.push_back(in.get());
+            mc = 0;
+            pc = 0;
+            core = 0;
+            break;
+        }
+        case l_undef:
+            if (m.canceled()) {
+                throw tactic_exception(Z3_CANCELED_MSG);
+            }
+            throw tactic_exception(m_solver->reason_unknown().c_str());
+        }
+        m_solver->pop(1);
+    }
+
+    virtual void collect_statistics(statistics & st) const {
+        m_solver->collect_statistics(st);
+    }
+    virtual void reset_statistics() {}
+
+    virtual void cleanup() {
+        m_solver = m_solver->translate(m, m_params);
+    }
+    virtual void reset() { cleanup(); }
+
+    virtual void set_logic(symbol const & l) {}
+
+    virtual void set_progress_callback(progress_callback * callback) {
+        m_solver->set_progress_callback(callback);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(solver2tactic, m_solver->translate(m, m_params));
+    }    
+};
+
+tactic* mk_solver2tactic(solver* s) { return alloc(solver2tactic, s); }
diff --git a/src/solver/solver2tactic.h b/src/solver/solver2tactic.h
new file mode 100644
index 000000000..65fbd37b1
--- /dev/null
+++ b/src/solver/solver2tactic.h
@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    solver2tactic.h
+
+Abstract:
+
+    Convert solver to a tactic.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-10-17
+
+Notes:
+   
+--*/
+#ifndef SOLVER2TACTIC_H_
+#define SOLVER2TACTIC_H_
+
+#include "tactic.h"
+#include "filter_model_converter.h"
+class solver;
+
+tactic * mk_solver2tactic(solver* s);
+
+void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, obj_map<expr, expr*>& bool2dep, ref<filter_model_converter>& fmc);
+
+#endif
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index f53301948..213ba5c1c 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -160,6 +160,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
         }
     }
     catch (z3_error & ex) {
+        TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
         throw ex;
     }
     catch (z3_exception & ex) {
diff --git a/src/tactic/arith/bound_manager.cpp b/src/tactic/arith/bound_manager.cpp
index ed77467c3..97d93658c 100644
--- a/src/tactic/arith/bound_manager.cpp
+++ b/src/tactic/arith/bound_manager.cpp
@@ -79,12 +79,23 @@ static bool is_strict(decl_kind k) {
     return k == OP_LT || k == OP_GT;
 } 
 
+bool bound_manager::is_numeral(expr* v, numeral& n, bool& is_int) {
+    expr* w;
+    if (m_util.is_uminus(v, w) && is_numeral(w, n, is_int)) {
+        n.neg();
+        return true;
+    }
+    return m_util.is_numeral(v, n, is_int);
+}
+
 void bound_manager::operator()(expr * f, expr_dependency * d) {
     TRACE("bound_manager", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";);
     expr * v;
     numeral n;
     if (is_disjunctive_bound(f, d))
         return;
+    if (is_equality_bound(f, d))
+        return;
     bool pos = true;    
     while (m().is_not(f, f))
         pos = !pos;
@@ -99,10 +110,10 @@ void bound_manager::operator()(expr * f, expr_dependency * d) {
     expr * lhs = t->get_arg(0);
     expr * rhs = t->get_arg(1);
     bool is_int;
-    if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, n, is_int)) {
+    if (is_uninterp_const(lhs) && is_numeral(rhs, n, is_int)) {
         v = lhs;
     }
-    else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, n, is_int)) {
+    else if (is_uninterp_const(rhs) && is_numeral(lhs, n, is_int)) {
         v = rhs;
         k = swap_decl(k);
     }
@@ -165,6 +176,26 @@ void bound_manager::insert_lower(expr * v, bool strict, numeral const & n, expr_
     }
 }
 
+bool bound_manager::is_equality_bound(expr * f, expr_dependency * d) {
+    expr* x, *y;
+    if (!m().is_eq(f, x, y)) {
+        return false;
+    }
+    if (!is_uninterp_const(x)) {
+        std::swap(x, y);
+    }
+    numeral n;
+    bool is_int;
+    if (is_uninterp_const(x) && is_numeral(y, n, is_int)) {
+        insert_lower(x, false, n, d);
+        insert_upper(x, false, n, d);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
 bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) {
     numeral lo, hi, n;
     if (!m().is_or(f)) return false;
@@ -176,14 +207,14 @@ bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) {
         expr * e = to_app(f)->get_arg(i);
         if (!m().is_eq(e, x, y)) return false;
         if (is_uninterp_const(x) && 
-            m_util.is_numeral(y, n, is_int) && is_int && 
+            is_numeral(y, n, is_int) && is_int && 
             (x == v || v == 0)) {
             if (v == 0) { v = x; lo = hi = n; }
             if (n < lo) lo = n;
             if (n > hi) hi = n;
         }
         else if (is_uninterp_const(y) && 
-                 m_util.is_numeral(x, n, is_int) && is_int && 
+                 is_numeral(x, n, is_int) && is_int && 
                  (y == v || v == 0)) {
             if (v == 0) { v = y; lo = hi = n; }
             if (n < lo) lo = n;
diff --git a/src/tactic/arith/bound_manager.h b/src/tactic/arith/bound_manager.h
index cc0d693e9..6a4dc2c96 100644
--- a/src/tactic/arith/bound_manager.h
+++ b/src/tactic/arith/bound_manager.h
@@ -36,6 +36,8 @@ private:
     obj_map<expr, expr_dependency*> m_upper_deps;
     ptr_vector<expr>     m_bounded_vars;
     bool is_disjunctive_bound(expr * f, expr_dependency * d);
+    bool is_equality_bound(expr * f, expr_dependency * d);
+    bool is_numeral(expr* v, rational& n, bool& is_int);
     void insert_lower(expr * v, bool strict, numeral const & n, expr_dependency * d);
     void insert_upper(expr * v, bool strict, numeral const & n, expr_dependency * d);
 public:
diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
index d8b016d7b..46b5a51b0 100644
--- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp
+++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
@@ -59,6 +59,7 @@ Revision History:
 #include "model_smt2_pp.h"
 #include "expr_safe_replace.h"
 #include "ast_util.h"
+#include "solver2tactic.h"
 
 class nl_purify_tactic : public tactic {
 
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index f7236351c..688d9403a 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -251,6 +251,16 @@ private:
                 }
                 sub.insert(e, t);
             }
+            else {
+                IF_VERBOSE(1, 
+                           verbose_stream() << "unprocessed entry: " << mk_pp(e, m) << "\n";
+                           if (bm.has_lower(e, lo, s1)) {
+                               verbose_stream() << "lower: " << lo << " " << s1 << "\n";
+                           } 
+                           if (bm.has_upper(e, hi, s2)) {
+                               verbose_stream() << "upper: " << hi << " " << s2 << "\n";
+                           });
+            }
         }
     }
 
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 81825221e..d2414ec72 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -40,6 +40,7 @@ Notes:
 #include"inc_sat_solver.h"
 #include"fd_solver.h"
 #include"bv_rewriter.h"
+#include"solver2tactic.h"
 
 
 tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
@@ -89,6 +90,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
         return mk_qffpbv_tactic(m, p);
     else if (logic=="HORN")
         return mk_horn_tactic(m, p);
+    else if (logic == "QF_FD")
+        return mk_solver2tactic(mk_fd_solver(m, p));
     //else if (logic=="QF_UFNRA")
     //    return mk_qfufnra_tactic(m, p);
     else 
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index 0f5d2838e..9e35d6e8b 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -202,7 +202,8 @@ Notes:
                 return ge(full, k, n, in.c_ptr());
             }
             else if (k == 1) {
-                return mk_at_most_1(full, n, xs);
+                literal_vector ors;
+                return mk_at_most_1(full, n, xs, ors);
             }
             else {
                 SASSERT(2*k <= n);
@@ -221,6 +222,9 @@ Notes:
             if (dualize(k, n, xs, in)) {
                 return eq(k, n, in.c_ptr());
             }
+            else if (k == 1) {
+                return mk_exactly_1(true, n, xs);
+            }
             else {
                 SASSERT(2*k <= n);
                 m_t = EQ;
@@ -238,12 +242,56 @@ Notes:
         
     private:
 
-        literal mk_at_most_1(bool full, unsigned n, literal const* xs) {
+
+        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) {
+            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) {
+            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) {
+                return ors[0];
+            }
+            literal result = fresh();
+            mk_implies_or(result, ors.size(), ors.c_ptr());
+            mk_or_implies(result, ors.size(), ors.c_ptr());
+            return result;
+        }
+
+        literal mk_exactly_1(bool full, unsigned n, literal const* xs) {
+            literal_vector ors;
+            literal r1 = mk_at_most_1(full, n, xs, ors);
+
+            if (full) {
+                r1 = mk_and(r1, mk_or(ors));
+            }
+            else {
+                mk_implies_or(r1, ors.size(), ors.c_ptr());
+            }
+            return r1;
+        }
+
+        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 (!full && n >= 4) {
+            if (false && !full && n >= 4) {
                 return mk_at_most_1_bimander(n, xs);
             }
             literal_vector in(n, xs);
@@ -252,9 +300,10 @@ Notes:
             literal_vector ands;
             ands.push_back(result);
             while (!in.empty()) {
-                literal_vector ors;
+                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);
@@ -267,7 +316,6 @@ Notes:
                 }
                 in.reset();
                 in.append(ors);
-                ors.reset();                
             }
             if (full) {
                 add_clause(ands);
@@ -278,23 +326,16 @@ Notes:
         void mk_at_most_1_small(bool full, bool last, unsigned n, literal const* xs, literal result, literal_vector& ands, literal_vector& ors) {
             SASSERT(n > 0);
             if (n == 1) {
-                if (!last) {
-                    ors.push_back(xs[0]);
-                }
+                ors.push_back(xs[0]);                
                 return;
             }
-            if (!last) {
-                literal ex = fresh();
-                for (unsigned j = 0; j < n; ++j) {
-                    add_clause(ctx.mk_not(xs[j]), ex);
-                }
-                if (full) {
-                    literal_vector lits(n, xs);
-                    lits.push_back(ctx.mk_not(ex));
-                    add_clause(lits.size(), lits.c_ptr());
-                }
-                ors.push_back(ex);
+            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) {
                 for (unsigned j = i + 1; j < n; ++j) {

From da4289fadc378f5cc601abeb5e37176ed16c9b8a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 25 Oct 2016 20:47:48 -0700
Subject: [PATCH 09/22] fix unit tests for pb

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/pb2bv_rewriter.cpp | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 8871c3dd8..0cae3f307 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -140,10 +140,17 @@ struct pb2bv_rewriter::imp {
             case l_true: 
                 return mk_and(fmls);
             case l_false:
-                fmls.push_back(bv.mk_ule(bound, es.back()));
+                if (!es.empty()) {
+                    fmls.push_back(bv.mk_ule(bound, es.back()));
+                }
                 return mk_or(fmls);
             case l_undef:
-                fmls.push_back(m.mk_eq(bound, es.back()));
+                if (es.empty()) {
+                    fmls.push_back(m.mk_bool_val(k.is_zero()));
+                }
+                else {
+                    fmls.push_back(m.mk_eq(bound, es.back()));
+                }
                 return mk_and(fmls);
             default:
                 UNREACHABLE();

From 86285e1641c8339e23edddf1236afc7f2253ac7a Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 26 Oct 2016 12:59:26 +0100
Subject: [PATCH 10/22] disabled unnecessary assertion

---
 scripts/mk_util.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index a86499149..0fac30e35 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -3278,7 +3278,7 @@ class MakeRuleCmd(object):
             #print("WARNING: Generating makefile rule that {}s {} '{}' which is outside the installation prefix '{}'.".format(
             #        action_string, 'to' if is_install else 'from', path, PREFIX))
         else:
-            assert not os.path.isabs(path)
+            # assert not os.path.isabs(path)
             install_root = cls.install_root()
         return install_root
 

From ead970b4778330768e64a04f13a46289f974cb85 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 26 Oct 2016 14:08:33 +0100
Subject: [PATCH 11/22] Bugfix for Python API.

Thanks to John D. Ramsdell for reporting this issue (http://stackoverflow.com/questions/39584779/why-is-the-sort-of-a-bound-variable-forced-not-to-be-a-finite-domain-sort).
---
 src/api/python/z3/z3.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 514a45fc6..b9d7f6df0 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -1817,7 +1817,7 @@ class QuantifierRef(BoolRef):
         """
         if __debug__:
             _z3_assert(idx < self.num_vars(), "Invalid variable idx")
-        return SortRef(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
+        return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
 
     def children(self):
         """Return a list containing a single element self.body()

From e381cef92ca88e48a875d3da1a4cb3cb32206352 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 26 Oct 2016 15:12:10 +0100
Subject: [PATCH 12/22] Marked .NET Z3Exception as serializable

---
 src/api/dotnet/Z3Exception.cs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/api/dotnet/Z3Exception.cs b/src/api/dotnet/Z3Exception.cs
index adda43995..71e4fef1a 100644
--- a/src/api/dotnet/Z3Exception.cs
+++ b/src/api/dotnet/Z3Exception.cs
@@ -14,7 +14,7 @@ Author:
     Christoph Wintersteiger (cwinter) 2012-03-15
 
 Notes:
-    
+
 --*/
 
 using System;
@@ -24,6 +24,7 @@ namespace Microsoft.Z3
   /// <summary>
   /// The exception base class for error reporting from Z3
   /// </summary>
+  [Serializable]
   public class Z3Exception : Exception
   {
     /// <summary>

From bea7bc5e30170694af655bc244a4dd9b8da1b2d8 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 26 Oct 2016 16:32:44 +0100
Subject: [PATCH 13/22] Bugfix for bv2fpa_converter. Fixes #767.

---
 src/ast/fpa/bv2fpa_converter.cpp | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp
index 07a24e40a..0dec98e5c 100644
--- a/src/ast/fpa/bv2fpa_converter.cpp
+++ b/src/ast/fpa/bv2fpa_converter.cpp
@@ -322,10 +322,17 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
         v2 = mc->get_const_interp(a2->get_decl());
 #else
         expr * bv = mc->get_const_interp(to_app(to_app(a0)->get_arg(0))->get_decl());
-        unsigned bv_sz = m_bv_util.get_bv_size(bv);
-        v0 = m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv);
-        v1 = m_bv_util.mk_extract(bv_sz-2, sbits-1, bv);
-        v2 = m_bv_util.mk_extract(sbits-2, 0, bv);
+        if (bv == 0) {
+            v0 = m_bv_util.mk_numeral(0, 1);
+            v1 = m_bv_util.mk_numeral(0, ebits);
+            v2 = m_bv_util.mk_numeral(0, sbits-1);
+        }
+        else {
+            unsigned bv_sz = m_bv_util.get_bv_size(bv);
+            v0 = m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv);
+            v1 = m_bv_util.mk_extract(bv_sz-2, sbits-1, bv);
+            v2 = m_bv_util.mk_extract(sbits-2, 0, bv);
+        }
 #endif
 
         if (!v0) v0 = m_bv_util.mk_numeral(0, 1);

From 4bd83724dddcc03c32ec5fa683590f2de631514d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 26 Oct 2016 19:15:05 -0700
Subject: [PATCH 14/22] remove conflict on false disequality, introduced
 regression

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_solver.cpp                |  4 +++-
 src/sat/sat_solver/inc_sat_solver.cpp | 21 ++++++++++++++-------
 src/smt/smt_context.cpp               |  3 ++-
 src/solver/solver2tactic.cpp          |  4 +---
 src/util/sorting_network.h            | 26 ++++++++++++++++++++++++++
 5 files changed, 46 insertions(+), 12 deletions(-)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index c3aaa5697..ab98fd8a0 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3168,7 +3168,8 @@ namespace sat {
             ++num_iterations;
             checkpoint();
             literal_set::iterator it = vars.begin(), end = vars.end();
-            for (; it != end; ++it) {
+            unsigned chunk_size = 100;
+            for (; it != end && chunk_size > 0; ++it) {
                 literal lit = *it;
                 if (value(lit) != l_undef) {
                     continue;
@@ -3182,6 +3183,7 @@ namespace sat {
                         return l_false;
                     }
                     propagate(false);
+                    --chunk_size;
                 }
             }
             lbool is_sat;
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index d091339bd..592603e53 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -257,10 +257,12 @@ public:
             bool_var2conseq.insert(lconseq[i][0].var(), i);
         }
         
-        // extract original fixed variables 
+        // extract original fixed variables
+        u_map<expr*> asm2dep;
+        extract_asm2dep(dep2asm, asm2dep);
         for (unsigned i = 0; i < vars.size(); ++i) {
             expr_ref cons(m);
-            if (extract_fixed_variable(dep2asm, vars[i], bool_var2conseq, lconseq, cons)) {
+            if (extract_fixed_variable(dep2asm, asm2dep, vars[i], bool_var2conseq, lconseq, cons)) {
                 conseq.push_back(cons);
             }
         }
@@ -378,7 +380,7 @@ private:
         if (!atoms.empty()) {
             std::stringstream strm;
             strm << "interpreted atoms sent to SAT solver " << atoms;
-            TRACE("sat", std::cout << strm.str() << "\n";);
+            TRACE("sat", tout << strm.str() << "\n";);
             IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
             set_reason_unknown(strm.str().c_str());
             return l_undef;
@@ -449,9 +451,7 @@ private:
         return internalized;
     }
 
-    bool extract_fixed_variable(dep2asm_t& dep2asm, expr* v, u_map<unsigned> const& bool_var2conseq, vector<sat::literal_vector> const& lconseq, expr_ref& conseq) {
-        u_map<expr*> asm2dep;
-        extract_asm2dep(dep2asm, asm2dep);
+    bool extract_fixed_variable(dep2asm_t& dep2asm, u_map<expr*>& asm2dep, expr* v, u_map<unsigned> const& bool_var2conseq, vector<sat::literal_vector> const& lconseq, expr_ref& conseq) {
 
         sat::bool_var_vector bvars;
         if (!internalize_var(v, bvars)) {
@@ -484,6 +484,7 @@ private:
         return true;
     }
 
+    vector<rational> m_exps;
     void internalize_value(sat::literal_vector const& value, expr* v, expr_ref& val) {
         bv_util bvutil(m);
         if (is_uninterp_const(v) && m.is_bool(v)) {
@@ -492,10 +493,16 @@ private:
         }
         else if (is_uninterp_const(v) && bvutil.is_bv_sort(m.get_sort(v))) {
             SASSERT(value.size() == bvutil.get_bv_size(v));
+            if (m_exps.empty()) {
+                m_exps.push_back(rational::one());
+            }
+            while (m_exps.size() < value.size()) {
+                m_exps.push_back(rational(2)*m_exps.back());
+            }
             rational r(0);
             for (unsigned i = 0; i < value.size(); ++i) {
                 if (!value[i].sign()) {
-                    r += rational(2).expt(i);
+                    r += m_exps[i];
                 }
             }
             val = m.mk_eq(v, bvutil.mk_numeral(r, value.size()));
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 832d4dac7..027790da8 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1111,7 +1111,8 @@ namespace smt {
 
         if (r1 == r2) {
             TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
-            return false; // context is inconsistent
+            return true;
+            // return false; // context is inconsistent
         }
 
         // Propagate disequalities to theories
diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
index 53b120fea..8646d4813 100644
--- a/src/solver/solver2tactic.cpp
+++ b/src/solver/solver2tactic.cpp
@@ -160,9 +160,7 @@ public:
     }
     virtual void reset_statistics() {}
 
-    virtual void cleanup() {
-        m_solver = m_solver->translate(m, m_params);
-    }
+    virtual void cleanup() { }
     virtual void reset() { cleanup(); }
 
     virtual void set_logic(symbol const & l) {}
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index 9e35d6e8b..df3428ef3 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -251,6 +251,15 @@ Notes:
             return result;
         }
 
+#if 0
+        literal mk_and(literal_vector const& lits) {
+            if (lits.size() == 1) {
+                return lits[0];
+            }
+            
+        }
+#endif
+
         void mk_implies_or(literal l, unsigned n, literal const* xs) {
             literal_vector lits(n, xs);
             lits.push_back(ctx.mk_not(l));
@@ -337,11 +346,28 @@ Notes:
             ors.push_back(ex);                
             
             // result => xs[0] + ... + xs[n-1] <= 1
+#if 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]));
                 }
             }            
+#else
+            literal_vector atm;
+            for (unsigned i = 0; i < n; ++i) {
+                // at => !xs[1] & .. & !xs[i-1] & !xs[i+1] & ... & !xs[n-1] 
+                literal at = fresh();
+                for (unsigned j = 0; j < n; ++j) {
+                    if (i != j) {
+                        add_clause(ctx.mk_not(at), ctx.mk_not(xs[j]));
+                    }
+                }
+                atm.push_back(at);
+            }            
+            atm.push_back(ctx.mk_not(result));
+            add_clause(atm);
+
+#endif
             // xs[0] + ... + xs[n-1] <= 1 => and_x
             if (full) {
                 literal and_i = fresh();

From 24fc19ed5833ee19b748ab954b890768dd80d114 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Oct 2016 08:15:39 -0700
Subject: [PATCH 15/22] speed up consequence finding by avoiding local search
 whenver assumption level is reached during the initial phase

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/pb2bv_rewriter.cpp   |  7 +++++++
 src/ast/rewriter/pb2bv_rewriter.h     |  1 +
 src/cmd_context/cmd_context.cpp       |  2 +-
 src/sat/sat_solver.cpp                | 18 ++++++++++++------
 src/solver/combined_solver.cpp        |  8 +++++++-
 src/tactic/portfolio/pb2bv_solver.cpp |  2 +-
 6 files changed, 29 insertions(+), 9 deletions(-)

diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 0cae3f307..cf5b67793 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -433,6 +433,9 @@ 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());
     }
@@ -469,9 +472,13 @@ 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); } 
 unsigned pb2bv_rewriter::num_translated() const { return m_imp->m_num_translated; }
 
+
 void pb2bv_rewriter::collect_statistics(statistics & st) const { m_imp->collect_statistics(st); }
diff --git a/src/ast/rewriter/pb2bv_rewriter.h b/src/ast/rewriter/pb2bv_rewriter.h
index 47d8361cb..569eaf07d 100644
--- a/src/ast/rewriter/pb2bv_rewriter.h
+++ b/src/ast/rewriter/pb2bv_rewriter.h
@@ -36,6 +36,7 @@ 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/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index b7c80f65a..930a8fc71 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -736,7 +736,7 @@ bool cmd_context::set_logic(symbol const & s) {
 
 std::string cmd_context::reason_unknown() const {
     if (m_check_sat_result.get() == 0)
-        throw cmd_exception("state of the most recent check-sat command is not unknown");
+        throw cmd_exception("state of the most recent check-sat command is not known");
     return m_check_sat_result->reason_unknown();
 }
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index ab98fd8a0..831eb228f 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3168,8 +3168,8 @@ namespace sat {
             ++num_iterations;
             checkpoint();
             literal_set::iterator it = vars.begin(), end = vars.end();
-            unsigned chunk_size = 100;
-            for (; it != end && chunk_size > 0; ++it) {
+            unsigned num_resolves = 0;
+            for (; it != end; ++it) {
                 literal lit = *it;
                 if (value(lit) != l_undef) {
                     continue;
@@ -3182,16 +3182,22 @@ namespace sat {
                         TRACE("sat", tout << "inconsistent\n";);
                         return l_false;
                     }
-                    propagate(false);
-                    --chunk_size;
+                    propagate(false);                    
+                    ++num_resolves;
+                }
+                if (scope_lvl() == 1) {
+                    break;
                 }
             }
             lbool is_sat;
             while (true) {
+                if (scope_lvl() == 1 && num_resolves > 0) {
+                    is_sat = l_undef;
+                    break;
+                }
                 is_sat = bounded_search();
                 if (is_sat == l_undef) {
-                    restart();                  
-                    continue;
+                    restart();      
                 }
                 break;
             }
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 2856315bd..b03de70a2 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -197,7 +197,13 @@ public:
     virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
         switch_inc_mode();
         m_use_solver1_results = false;
-        return m_solver2->get_consequences(asms, vars, consequences);
+        try {
+            return m_solver2->get_consequences(asms, vars, consequences);
+        }
+        catch (z3_exception& ex) {
+            set_reason_unknown(ex.msg());
+        }
+        return l_undef;
     }
 
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index bfd533e8a..d1826e61d 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(m_assertions[i].get(), fml, proof);
+            m_rewriter.assert_expr(m_assertions[i].get(), fml, proof);
             m_solver->assert_expr(fml);
         }
         m_rewriter.flush_side_constraints(fmls);

From 41deae52c6018076a669739ed7c7b07bff381a21 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Oct 2016 13:35:53 -0700
Subject: [PATCH 16/22] fix enum2bv to handle singleton enumeration types,
 differentiate disequality conflicts for theories that handle disequalities
 vs. theories that don't

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/enum2bv_rewriter.cpp |  4 ++--
 src/smt/smt_context.cpp               |  4 ++--
 src/util/sorting_network.h            | 25 -------------------------
 3 files changed, 4 insertions(+), 29 deletions(-)

diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index bbe07f625..cd0f54503 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -126,7 +126,7 @@ struct enum2bv_rewriter::imp {
                 unsigned nc = m_dt.get_datatype_num_constructors(s);
                 result = m.mk_fresh_const(f->get_name().str().c_str(), m_bv.mk_sort(bv_size));
                 f_fresh = to_app(result)->get_decl();
-                if (!is_power_of_two(nc)) {
+                if (!is_power_of_two(nc) || nc == 1) {
                     m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size)));
                 }                
                 expr_ref f_def(m);
@@ -168,7 +168,7 @@ struct enum2bv_rewriter::imp {
                     unsigned bv_size = get_bv_size(s);
                     m_sorts.push_back(m_bv.mk_sort(bv_size));
                     unsigned nc = m_dt.get_datatype_num_constructors(s);
-                    if (!is_power_of_two(nc)) {
+                    if (!is_power_of_two(nc) || nc == 1) {
                         bounds.push_back(m_bv.mk_ule(m.mk_var(q->get_num_decls()-i-1, m_sorts[i]), m_bv.mk_numeral(nc-1, bv_size)));
                     }                
                     found = true;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 027790da8..fed6e71bc 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1111,8 +1111,8 @@ namespace smt {
 
         if (r1 == r2) {
             TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
-            return true;
-            // return false; // context is inconsistent
+            theory_id  t1 = r1->m_th_var_list.get_th_id();
+            return get_theory(t1)->use_diseqs();
         }
 
         // Propagate disequalities to theories
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index df3428ef3..33c4f8b61 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -251,15 +251,6 @@ Notes:
             return result;
         }
 
-#if 0
-        literal mk_and(literal_vector const& lits) {
-            if (lits.size() == 1) {
-                return lits[0];
-            }
-            
-        }
-#endif
-
         void mk_implies_or(literal l, unsigned n, literal const* xs) {
             literal_vector lits(n, xs);
             lits.push_back(ctx.mk_not(l));
@@ -346,28 +337,12 @@ Notes:
             ors.push_back(ex);                
             
             // result => xs[0] + ... + xs[n-1] <= 1
-#if 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]));
                 }
             }            
-#else
-            literal_vector atm;
-            for (unsigned i = 0; i < n; ++i) {
-                // at => !xs[1] & .. & !xs[i-1] & !xs[i+1] & ... & !xs[n-1] 
-                literal at = fresh();
-                for (unsigned j = 0; j < n; ++j) {
-                    if (i != j) {
-                        add_clause(ctx.mk_not(at), ctx.mk_not(xs[j]));
-                    }
-                }
-                atm.push_back(at);
-            }            
-            atm.push_back(ctx.mk_not(result));
-            add_clause(atm);
 
-#endif
             // xs[0] + ... + xs[n-1] <= 1 => and_x
             if (full) {
                 literal and_i = fresh();

From 7d7e03e377f1087202a8728fe0ee77b5d88b33ce Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Oct 2016 16:23:33 -0700
Subject: [PATCH 17/22] rewind qhead to ensure re-propagation after
 cancellation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_consequences.cpp | 1 +
 src/smt/smt_context.cpp      | 8 ++++++--
 src/util/rlimit.cpp          | 1 +
 3 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index ef90aac4c..1c1d236ad 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -258,6 +258,7 @@ namespace smt {
             TRACE("context", tout << is_sat << "\n";);
             return is_sat;
         }
+
         obj_map<expr, expr*> var2val;
         index_set _assumptions;
         for (unsigned i = 0; i < assumptions.size(); ++i) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index fed6e71bc..154f3a6a3 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1749,8 +1749,10 @@ namespace smt {
             unsigned qhead = m_qhead;
             if (!bcp())
                 return false;
-            if (get_cancel_flag()) 
+            if (get_cancel_flag()) {
+                m_qhead = qhead;
                 return true;
+            }
             SASSERT(!inconsistent());
             propagate_relevancy(qhead);
             if (inconsistent()) 
@@ -1768,8 +1770,10 @@ namespace smt {
             m_qmanager->propagate();
             if (inconsistent())
                 return false;
-            if (resource_limits_exceeded())
+            if (resource_limits_exceeded()) {
+                m_qhead = qhead;
                 return true;
+            }
             if (!can_propagate()) {
                 CASSERT("diseq_bug", inconsistent() || check_missing_diseq_conflict());
                 CASSERT("eqc_bool", check_eqc_bool_assignment());
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index 37b1f7904..9f6c692cc 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -29,6 +29,7 @@ uint64 reslimit::count() const {
     return m_count;
 }
 
+
 bool reslimit::inc() {
     ++m_count;
     return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);

From b1d673e3ebf7125c40144372f4747c71648fcae1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Oct 2016 16:34:26 -0700
Subject: [PATCH 18/22] catch cancellation exceptions, return undef

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/solver/combined_solver.cpp |  8 +++++++-
 src/solver/solver.cpp          | 16 +++++++++++++++-
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index b03de70a2..7f5f6872e 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -21,6 +21,7 @@ Notes:
 #include"solver.h"
 #include"scoped_timer.h"
 #include"combined_solver_params.hpp"
+#include"common_msgs.h"
 #define PS_VB_LVL 15
 
 /**
@@ -201,7 +202,12 @@ public:
             return m_solver2->get_consequences(asms, vars, consequences);
         }
         catch (z3_exception& ex) {
-            set_reason_unknown(ex.msg());
+            if (get_manager().canceled()) {
+                set_reason_unknown(Z3_CANCELED_MSG);
+            }
+            else {
+                set_reason_unknown(ex.msg());
+            }
         }
         return l_undef;
     }
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 8f32019d5..441ece429 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -21,6 +21,8 @@ Notes:
 #include"ast_util.h"
 #include"ast_pp.h"
 #include"ast_pp_util.h"
+#include "common_msgs.h"
+
 
 unsigned solver::get_num_assertions() const {
     NOT_IMPLEMENTED_YET();
@@ -56,7 +58,19 @@ struct scoped_assumption_push {
 };
 
 lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
-    return get_consequences_core(asms, vars, consequences);
+    try {
+        return get_consequences_core(asms, vars, consequences);
+    }
+    catch (z3_exception& ex) {
+        if (asms.get_manager().canceled()) {
+            set_reason_unknown(Z3_CANCELED_MSG);
+            return l_undef;
+        }
+        else {
+            set_reason_unknown(ex.msg());
+        }
+        throw;
+    }
 }
 
 lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {

From ca309341c3de0e3762acf663263e9cbc8b69eabb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Oct 2016 22:07:46 -0700
Subject: [PATCH 19/22] fixing cancellation code paths for inc_sat_solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 .../bit_blaster/bit_blaster_rewriter.cpp      |  9 ++++++
 .../bit_blaster/bit_blaster_rewriter.h        |  1 +
 src/sat/sat_solver.cpp                        | 29 ++++++++++++-------
 src/sat/sat_solver/inc_sat_solver.cpp         | 14 ++++++---
 .../portfolio/bounded_int2bv_solver.cpp       |  3 +-
 5 files changed, 41 insertions(+), 15 deletions(-)

diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index c260178ad..e8d8c4e4b 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -165,6 +165,10 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
         m_keyval_lim.push_back(m_keys.size());
     }
 
+    unsigned get_num_scopes() const {
+        return m_keyval_lim.size();
+    }
+
     void pop(unsigned num_scopes) {
         if (num_scopes > 0) {
             SASSERT(num_scopes <= m_keyval_lim.size());
@@ -637,6 +641,7 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
     }
     void push() { m_cfg.push(); }
     void pop(unsigned s) { m_cfg.pop(s); }
+    unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); }
 };
 
 bit_blaster_rewriter::bit_blaster_rewriter(ast_manager & m, params_ref const & p):
@@ -680,3 +685,7 @@ void bit_blaster_rewriter::operator()(expr * e, expr_ref & result, proof_ref & r
     m_imp->operator()(e, result, result_proof);
 }
 
+unsigned bit_blaster_rewriter::get_num_scopes() const {
+    return m_imp->get_num_scopes();
+}
+
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
index b23daab3a..8db328ec8 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
@@ -37,6 +37,7 @@ public:
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
     void push();
     void pop(unsigned num_scopes);
+    unsigned get_num_scopes() const;
 };
 
 #endif
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 831eb228f..e70a30a5a 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3158,7 +3158,14 @@ namespace sat {
         init_search();
         propagate(false);
         if (inconsistent()) return l_false;
-        init_assumptions(asms.size(), asms.c_ptr(), 0, 0);
+        if (asms.empty()) {
+            bool_var v = mk_var(true, false);
+            literal lit(v, false);
+            init_assumptions(1, &lit, 0, 0);
+        }
+        else {
+            init_assumptions(asms.size(), asms.c_ptr(), 0, 0);
+        }
         propagate(false);
         if (check_inconsistent()) return l_false;
        
@@ -3169,6 +3176,7 @@ namespace sat {
             checkpoint();
             literal_set::iterator it = vars.begin(), end = vars.end();
             unsigned num_resolves = 0;
+            lbool is_sat = l_true;
             for (; it != end; ++it) {
                 literal lit = *it;
                 if (value(lit) != l_undef) {
@@ -3179,8 +3187,10 @@ namespace sat {
                 propagate(false);
                 while (inconsistent()) {      
                     if (!resolve_conflict()) {
-                        TRACE("sat", tout << "inconsistent\n";);
-                        return l_false;
+                        TRACE("sat", display(tout << "inconsistent\n"););
+                        m_inconsistent = false;
+                        is_sat = l_undef;
+                        break;
                     }
                     propagate(false);                    
                     ++num_resolves;
@@ -3189,17 +3199,16 @@ namespace sat {
                     break;
                 }
             }
-            lbool is_sat;
-            while (true) {
+            if (is_sat == l_true) {
                 if (scope_lvl() == 1 && num_resolves > 0) {
                     is_sat = l_undef;
-                    break;
                 }
-                is_sat = bounded_search();
-                if (is_sat == l_undef) {
-                    restart();      
+                else {
+                    is_sat = bounded_search();
+                    if (is_sat == l_undef) {
+                        restart();      
+                    }
                 }
-                break;
             }
             if (is_sat == l_false) {
                 TRACE("sat", tout << "unsat\n";);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 592603e53..f5efed726 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -234,6 +234,7 @@ public:
     }
 
     virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
+        init_preprocess();
         TRACE("sat", tout << assumptions << "\n" << vars << "\n";);
         sat::literal_vector asms;
         sat::bool_var_vector bvars;
@@ -341,7 +342,7 @@ public:
                      mk_bit_blaster_tactic(m, m_bb_rewriter.get()),
                      //mk_aig_tactic(),
                      using_params(mk_simplify_tactic(m), simp2_p));
-        for (unsigned i = 0; i < m_num_scopes; ++i) {
+        while (m_bb_rewriter->get_num_scopes() < m_num_scopes) {
             m_bb_rewriter->push();
         }
         m_preprocess->reset();
@@ -364,6 +365,7 @@ private:
         }
         catch (tactic_exception & ex) {
             IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
+            TRACE("sat", tout << "exception: " << ex.msg() << "\n";);
             m_preprocess = 0;
             m_bb_rewriter = 0;
             return l_undef;
@@ -518,10 +520,14 @@ private:
         }
         dep2asm_t dep2asm;
         goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
-        for (; m_fmls_head < m_fmls.size(); ++m_fmls_head) {
-            g->assert_expr(m_fmls[m_fmls_head].get());
+        for (unsigned i = 0 ; i < m_fmls.size(); ++i) {
+            g->assert_expr(m_fmls[i].get());
         }
-        return internalize_goal(g, dep2asm);
+        lbool res = internalize_goal(g, dep2asm);
+        if (res != l_undef) {
+            m_fmls_head = m_fmls.size();
+        }
+        return res;
     }
 
     void extract_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index 688d9403a..f8b2f5325 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -247,8 +247,9 @@ private:
                 expr_ref t(m.mk_const(fbv), m);
                 t = m_bv.mk_bv2int(t);
                 if (!offset.is_zero()) {
-                    t = m_arith.mk_add(t, m_arith.mk_numeral(lo, true));
+                    t = m_arith.mk_add(t, m_arith.mk_numeral(offset, true));
                 }
+                TRACE("pb", tout << lo << " <= " << hi << " offset: " << offset << "\n"; tout << mk_pp(e, m) << " |-> " << t << "\n";);
                 sub.insert(e, t);
             }
             else {

From 6fb358a432ef411341cc18202a52da749dbd76f5 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 28 Oct 2016 13:45:10 +0100
Subject: [PATCH 20/22] Build fix for libz3.vcxproj.

---
 scripts/mk_util.py | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 0fac30e35..84931b47e 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -3076,6 +3076,11 @@ def mk_vs_proj_property_groups(f, name, target_ext, type):
     f.write('    <CharacterSet>Unicode</CharacterSet>\n')
     f.write('    <UseOfMfc>false</UseOfMfc>\n')
     f.write('  </PropertyGroup>\n')
+    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'" Label="Configuration">\n')
+    f.write('    <ConfigurationType>%s</ConfigurationType>\n' % type)
+    f.write('    <CharacterSet>Unicode</CharacterSet>\n')
+    f.write('    <UseOfMfc>false</UseOfMfc>\n')
+    f.write('  </PropertyGroup>\n')
     f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n')
     f.write('  <ImportGroup Label="ExtensionSettings" />\n')
     f.write('   <ImportGroup Label="PropertySheets">\n')

From 02e1bae9cbf1dd386c9ee89631958292ad27e7e0 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 28 Oct 2016 14:22:27 +0100
Subject: [PATCH 21/22] whitespace

---
 .../portfolio/bounded_int2bv_solver.cpp       | 32 +++++++++----------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index f8b2f5325..8be0788e3 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -14,7 +14,7 @@ Author:
     Nikolaj Bjorner (nbjorner) 2016-10-23
 
 Notes:
-   
+
 --*/
 
 #include "bounded_int2bv_solver.h"
@@ -76,7 +76,7 @@ public:
     virtual solver* translate(ast_manager& m, params_ref const& p) {
         return alloc(bounded_int2bv_solver, m, p, m_solver->translate(m, p));
     }
-    
+
     virtual void assert_expr(expr * t) {
         m_assertions.push_back(t);
     }
@@ -89,7 +89,7 @@ public:
     }
 
     virtual void pop_core(unsigned n) {
-        m_assertions.reset();        
+        m_assertions.reset();
         m_solver->pop(n);
 
         if (n > 0) {
@@ -109,7 +109,7 @@ public:
 
         while (n > 0) {
             dealloc(m_bounds.back());
-            m_bounds.pop_back();            
+            m_bounds.pop_back();
             --n;
         }
     }
@@ -120,25 +120,25 @@ public:
     }
 
     virtual void updt_params(params_ref const & p) { m_solver->updt_params(p);  }
-    virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }    
+    virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
     virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
     virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback);  }
     virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); }
     virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
-    virtual void get_model(model_ref & mdl) { 
+    virtual void get_model(model_ref & mdl) {
         m_solver->get_model(mdl);
         if (mdl) {
             extend_model(mdl);
-            filter_model(mdl);            
+            filter_model(mdl);
         }
-    } 
+    }
     virtual proof * get_proof() { return m_solver->get_proof(); }
     virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
     virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
-    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) { 
+    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) {
         flush_assertions();
         expr_ref_vector bvars(m);
         for (unsigned i = 0; i < vars.size(); ++i) {
@@ -201,7 +201,7 @@ private:
                 value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true));
             }
             TRACE("int2bv", tout << mk_pp(it->m_key, m) << " " << value << "\n";);
-            ext.insert(it->m_key, value);            
+            ext.insert(it->m_key, value);
         }
         ext(mdl, 0);
     }
@@ -224,7 +224,7 @@ private:
             if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2) {
                 func_decl* fbv;
                 rational offset;
-                if (!m_int2bv.find(f, fbv)) {                    
+                if (!m_int2bv.find(f, fbv)) {
                     rational n = hi - lo + rational::one();
                     unsigned num_bits = get_num_bits(n);
                     expr_ref b(m);
@@ -253,11 +253,11 @@ private:
                 sub.insert(e, t);
             }
             else {
-                IF_VERBOSE(1, 
+                IF_VERBOSE(1,
                            verbose_stream() << "unprocessed entry: " << mk_pp(e, m) << "\n";
                            if (bm.has_lower(e, lo, s1)) {
                                verbose_stream() << "lower: " << lo << " " << s1 << "\n";
-                           } 
+                           }
                            if (bm.has_upper(e, hi, s2)) {
                                verbose_stream() << "upper: " << hi << " " << s2 << "\n";
                            });
@@ -284,7 +284,7 @@ private:
             bm(m_assertions[i].get());
         }
         expr_safe_replace sub(m);
-        accumulate_sub(sub);        
+        accumulate_sub(sub);
         proof_ref proof(m);
         expr_ref fml1(m), fml2(m);
         if (sub.empty()) {
@@ -292,7 +292,7 @@ private:
         }
         else {
             for (unsigned i = 0; i < m_assertions.size(); ++i) {
-                sub(m_assertions[i].get(), fml1);            
+                sub(m_assertions[i].get(), fml1);
                 m_rewriter(fml1, fml2, proof);
                 m_solver->assert_expr(fml2);
                 TRACE("int2bv", tout << fml2 << "\n";);

From f1412d3f3249529224f4180f601652da210b274a Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 28 Oct 2016 14:23:01 +0100
Subject: [PATCH 22/22] Bugfix for bouned_int2bv_solver

---
 src/tactic/portfolio/bounded_int2bv_solver.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index 8be0788e3..0b136dda7 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -294,6 +294,10 @@ private:
             for (unsigned i = 0; i < m_assertions.size(); ++i) {
                 sub(m_assertions[i].get(), fml1);
                 m_rewriter(fml1, fml2, proof);
+                if (m.canceled()) {
+                    m_rewriter.reset();
+                    return;
+                }
                 m_solver->assert_expr(fml2);
                 TRACE("int2bv", tout << fml2 << "\n";);
             }