diff --git a/examples/python/mus/marco.py b/examples/python/mus/marco.py
new file mode 100644
index 000000000..b6689636d
--- /dev/null
+++ b/examples/python/mus/marco.py
@@ -0,0 +1,185 @@
+############################################
+# Copyright (c) 2016 Microsoft Corporation
+# 
+# Basic core and correction set enumeration.
+#
+# Author: Nikolaj Bjorner (nbjorner)
+############################################
+
+"""
+Enumeration of Minimal Unsatisfiable Cores and Maximal Satisfying Subsets
+This tutorial illustrates how to use Z3 for extracting all minimal unsatisfiable
+cores together with all maximal satisfying subsets. 
+
+Origin
+The algorithm that we describe next represents the essence of the core extraction
+procedure by Liffiton and Malik and independently by Previti and Marques-Silva: 
+ Enumerating Infeasibility: Finding Multiple MUSes Quickly
+ Mark H. Liffiton and Ammar Malik
+ in Proc. 10th International Conference on Integration of Artificial Intelligence (AI)
+ and Operations Research (OR) techniques in Constraint Programming (CPAIOR-2013), 160-175, May 2013. 
+
+Partial MUS Enumeration
+ Alessandro Previti, Joao Marques-Silva in Proc. AAAI-2013 July 2013 
+
+Z3py Features
+
+This implementation contains no tuning. It was contributed by Mark Liffiton and it is
+a simplification of one of the versions available from his Marco Polo Web site.
+It illustrates the following features of Z3's Python-based API:
+   1. Using assumptions to track unsatisfiable cores. 
+   2. Using multiple solvers and passing constraints between them. 
+   3. Calling the C-based API from Python. Not all API functions are supported over the
+      Python wrappers. This example shows how to get a unique integer identifier of an AST,
+      which can be used as a key in a hash-table. 
+
+Idea of the Algorithm
+The main idea of the algorithm is to maintain two logical contexts and exchange information
+between them:
+
+    1. The MapSolver is used to enumerate sets of clauses that are not already
+       supersets of an existing unsatisfiable core and not already a subset of a maximal satisfying
+       assignment. The MapSolver uses one unique atomic predicate per soft clause, so it enumerates
+       sets of atomic predicates. For each minimal unsatisfiable core, say, represented by predicates
+       p1, p2, p5, the MapSolver contains the clause  !p1 | !p2 | !p5. For each maximal satisfiable
+       subset, say, represented by predicats p2, p3, p5, the MapSolver contains a clause corresponding
+       to the disjunction of all literals not in the maximal satisfiable subset, p1 | p4 | p6. 
+    2. The SubsetSolver contains a set of soft clauses (clauses with the unique indicator atom occurring negated).
+       The MapSolver feeds it a set of clauses (the indicator atoms). Recall that these are not already a superset
+       of an existing minimal unsatisfiable core, or a subset of a maximal satisfying assignment. If asserting
+       these atoms makes the SubsetSolver context infeasible, then it finds a minimal unsatisfiable subset
+       corresponding to these atoms. If asserting the atoms is consistent with the SubsetSolver, then it
+       extends this set of atoms maximally to a satisfying set. 
+"""
+
+from z3 import *
+
+def main():
+    x, y = Reals('x y')
+    constraints = [x > 2, x < 1, x < 0, Or(x + y > 0, y < 0), Or(y >= 0, x >= 0), Or(y < 0, x < 0), Or(y > 0, x < 0)]
+    csolver = SubsetSolver(constraints)
+    msolver = MapSolver(n=csolver.n)
+    for orig, lits in enumerate_sets(csolver, msolver):
+        output = "%s %s" % (orig, lits)
+        print(output)
+
+
+def get_id(x):
+    return Z3_get_ast_id(x.ctx.ref(),x.as_ast())
+
+
+class SubsetSolver:
+   constraints = []
+   n = 0
+   s = Solver()
+   varcache = {}
+   idcache = {}
+
+   def __init__(self, constraints):
+       self.constraints = constraints
+       self.n = len(constraints)
+       for i in range(self.n):
+           self.s.add(Implies(self.c_var(i), constraints[i]))
+
+   def c_var(self, i):
+       if i not in self.varcache:
+          v = Bool(str(self.constraints[abs(i)]))
+          self.idcache[get_id(v)] = abs(i)
+          if i >= 0:
+             self.varcache[i] = v
+          else:
+             self.varcache[i] = Not(v)
+       return self.varcache[i]
+
+   def check_subset(self, seed):
+       assumptions = self.to_c_lits(seed)
+       return (self.s.check(assumptions) == sat)
+        
+   def to_c_lits(self, seed):
+       return [self.c_var(i) for i in seed]
+
+   def complement(self, aset):
+       return set(range(self.n)).difference(aset)
+
+   def seed_from_core(self):
+       core = self.s.unsat_core()
+       return [self.idcache[get_id(x)] for x in core]
+
+   def shrink(self, seed):
+       current = set(seed)
+       for i in seed:
+          if i not in current:
+             continue
+          current.remove(i)
+          if not self.check_subset(current):
+             current = set(self.seed_from_core())
+          else:
+             current.add(i)
+       return current
+
+   def grow(self, seed):
+       current = seed
+       for i in self.complement(current):
+           current.append(i)
+           if not self.check_subset(current):
+              current.pop()
+       return current
+
+
+
+class MapSolver:
+   def __init__(self, n):
+       """Initialization.
+             Args:
+            n: The number of constraints to map.
+       """
+       self.solver = Solver()
+       self.n = n
+       self.all_n = set(range(n))  # used in complement fairly frequently
+
+   def next_seed(self):
+       """Get the seed from the current model, if there is one.
+            Returns:
+            A seed as an array of 0-based constraint indexes.
+       """
+       if self.solver.check() == unsat:
+            return None
+       seed = self.all_n.copy()  # default to all True for "high bias"
+       model = self.solver.model()
+       for x in model:
+           if is_false(model[x]):
+              seed.remove(int(x.name()))
+       return list(seed)
+
+   def complement(self, aset):
+       """Return the complement of a given set w.r.t. the set of mapped constraints."""
+       return self.all_n.difference(aset)
+
+   def block_down(self, frompoint):
+       """Block down from a given set."""
+       comp = self.complement(frompoint)
+       self.solver.add( Or( [Bool(str(i)) for i in comp] ) )
+
+   def block_up(self, frompoint):
+       """Block up from a given set."""
+       self.solver.add( Or( [Not(Bool(str(i))) for i in frompoint] ) )
+    
+
+
+def enumerate_sets(csolver, map):
+    """Basic MUS/MCS enumeration, as a simple example."""
+    while True:
+        seed = map.next_seed()
+        if seed is None:
+           return
+        if csolver.check_subset(seed):
+           MSS = csolver.grow(seed)
+           yield ("MSS", csolver.to_c_lits(MSS))
+           map.block_down(MSS)
+        else:
+           MUS = csolver.shrink(seed)
+           yield ("MUS", csolver.to_c_lits(MUS))
+           map.block_up(MUS)
+
+main()
+
diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
index 9634e17cb..ab21c4c88 100644
--- a/src/ast/array_decl_plugin.cpp
+++ b/src/ast/array_decl_plugin.cpp
@@ -522,7 +522,7 @@ void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol
 void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
     op_names.push_back(builtin_name("store",OP_STORE));
     op_names.push_back(builtin_name("select",OP_SELECT));
-    if (logic == symbol::null) {
+    if (logic == symbol::null || logic == symbol("HORN")) {
         // none of the SMT2 logics support these extensions
         op_names.push_back(builtin_name("const",OP_CONST_ARRAY));
         op_names.push_back(builtin_name("map",OP_ARRAY_MAP));
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index fd2535968..07e97364e 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -252,7 +252,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
         r2 = m_util.norm(r2, sz, is_signed);
 
     if (is_num1 && is_num2) {
-        result = r1 <= r2 ? m().mk_true() : m().mk_false();
+        result = m().mk_bool_val(r1 <= r2);
         return BR_DONE;
     }
 
@@ -1106,6 +1106,8 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
         return BR_DONE;
 }
 
+
+
 br_status bv_rewriter::mk_zero_extend(unsigned n, expr * arg, expr_ref & result) {
     if (n == 0) {
         result = arg;
@@ -1783,7 +1785,7 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
 
     if (is_numeral(lhs)) {
         SASSERT(is_numeral(rhs));
-        result = lhs == rhs ? m().mk_true() : m().mk_false();
+        result = m().mk_bool_val(lhs == rhs);
         return BR_DONE;
     }
 
@@ -2132,7 +2134,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
         st = cancel_monomials(lhs, rhs, false, new_lhs, new_rhs);
         if (st != BR_FAILED) {
             if (is_numeral(new_lhs) && is_numeral(new_rhs)) {
-                result = new_lhs == new_rhs ? m().mk_true() : m().mk_false();
+                result = m().mk_bool_val(new_lhs == new_rhs);
                 return BR_DONE;
             }
         }
@@ -2197,11 +2199,21 @@ br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args,
     unsigned bv_sz;
     rational a0_val, a1_val;
 
-    if (m_util.is_numeral(args[0], a0_val, bv_sz) &&
-        m_util.is_numeral(args[1], a1_val, bv_sz)) {
+    bool is_num1 = is_numeral(args[0], a0_val, bv_sz);
+    bool is_num2 = is_numeral(args[1], a1_val, bv_sz);
+    if (is_num1 && (a0_val.is_zero() || a0_val.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    if (is_num2 && (a1_val.is_zero() || a1_val.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+
+    if (is_num1 && is_num2) {
         rational mr = a0_val * a1_val;
         rational lim = rational::power_of_two(bv_sz-1);
-        result = (mr < lim) ? m().mk_true() : m().mk_false();
+        result = m().mk_bool_val(mr < lim);
         return BR_DONE;
     }
 
@@ -2213,11 +2225,21 @@ br_status bv_rewriter::mk_bvumul_no_overflow(unsigned num, expr * const * args,
     unsigned bv_sz;
     rational a0_val, a1_val;
 
-    if (m_util.is_numeral(args[0], a0_val, bv_sz) &&
-        m_util.is_numeral(args[1], a1_val, bv_sz)) {
+    bool is_num1 = is_numeral(args[0], a0_val, bv_sz);
+    bool is_num2 = is_numeral(args[1], a1_val, bv_sz);
+    if (is_num1 && (a0_val.is_zero() || a0_val.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    if (is_num2 && (a1_val.is_zero() || a1_val.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+
+    if (is_num1 && is_num2) {
         rational mr = a0_val * a1_val;
         rational lim = rational::power_of_two(bv_sz);
-        result = (mr < lim) ? m().mk_true() : m().mk_false();
+        result = m().mk_bool_val(mr < lim);
         return BR_DONE;
     }
 
@@ -2229,8 +2251,18 @@ br_status bv_rewriter::mk_bvsmul_no_underflow(unsigned num, expr * const * args,
     unsigned bv_sz;
     rational a0_val, a1_val;
 
-    if (m_util.is_numeral(args[0], a0_val, bv_sz) &&
-        m_util.is_numeral(args[1], a1_val, bv_sz)) {
+    bool is_num1 = is_numeral(args[0], a0_val, bv_sz);
+    bool is_num2 = is_numeral(args[1], a1_val, bv_sz);
+    if (is_num1 && (a0_val.is_zero() || a0_val.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    if (is_num2 && (a1_val.is_zero() || a1_val.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+
+    if (is_num1 && is_num2) {
         rational ul = rational::power_of_two(bv_sz);
         rational lim = rational::power_of_two(bv_sz-1);
         if (a0_val >= lim) a0_val -= ul;
@@ -2238,7 +2270,7 @@ br_status bv_rewriter::mk_bvsmul_no_underflow(unsigned num, expr * const * args,
         rational mr = a0_val * a1_val;
         rational neg_lim = -lim;
         TRACE("bv_rewriter_bvsmul_no_underflow", tout << "a0:" << a0_val << " a1:" << a1_val << " mr:" << mr << " neg_lim:" << neg_lim << std::endl;);
-        result = (mr >= neg_lim) ? m().mk_true() : m().mk_false();
+        result = m().mk_bool_val(mr >= neg_lim);
         return BR_DONE;
     }
 
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 219a4b45a..85371d8ef 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -454,8 +454,7 @@ public:
                     (*p)(model, vars, fmls);
                 }
             }
-            while (!vars.empty() && !fmls.empty()) {
-                std::cout << "mbp: " << var << "\n";
+            while (!vars.empty() && !fmls.empty()) {                
                 var = vars.back();
                 vars.pop_back();
                 project_plugin* p = get_plugin(var);
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 02c6d26cd..1bfd53597 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -158,6 +158,8 @@ namespace qe {
             return;
         }
         model_evaluator eval(*mdl);
+        eval.set_model_completion(true);
+        TRACE("qe", model_v2_pp(tout, *mdl););
 
         expr_ref val(m);
         for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) {
@@ -169,7 +171,7 @@ namespace qe {
             if (m.is_false(val)) {
                 m_asms.push_back(m.mk_not(p));
             }
-            else {
+            else {                
                 SASSERT(m.is_true(val));
                 m_asms.push_back(p);
             }
diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp
index adfe42192..81635f906 100644
--- a/src/solver/mus.cpp
+++ b/src/solver/mus.cpp
@@ -475,7 +475,6 @@ lbool mus::get_mus(expr_ref_vector& mus) {
     return m_imp->get_mus(mus);
 }
 
-
 void mus::reset() {
     m_imp->reset();
 }
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 56b246c1e..2a00d7195 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -23,6 +23,7 @@ Notes:
 #include"tactic.h"
 #include"ast_pp_util.h"
 #include"ast_translation.h"
+#include"mus.h"
 
 /**
    \brief Simulates the incremental solver interface using a tactic.
@@ -42,6 +43,7 @@ class tactic2solver : public solver_na2as {
     bool                         m_produce_proofs;
     bool                         m_produce_unsat_cores;
     statistics                   m_stats;
+    
 public:
     tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic);
     virtual ~tactic2solver();
@@ -203,8 +205,9 @@ void tactic2solver::collect_statistics(statistics & st) const {
 }
 
 void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
-    if (m_result.get())
+    if (m_result.get()) {
         m_result->get_unsat_core(r);
+    }
 }
 
 void tactic2solver::get_model(model_ref & m) {