diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 68122a941..05085a3d7 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -604,8 +604,16 @@ namespace z3 {
 
         /**
            \brief Return true if this expression is a numeral.
+           Specialized functions also return representations for the numerals as
+           small integers, 64 bit integers or rational or decimal strings.
         */
         bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
+        bool is_numeral_i64(__int64& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); return r;}
+        bool is_numeral_u64(__uint64& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); return r;}
+        bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); return r;}
+        bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); return r;}
+        bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); return true; }
+        bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); return true; }
         /**
            \brief Return true if this expression is an application.
         */
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 374c71be4..2cd50c181 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -3940,7 +3940,7 @@ class ArraySortRef(SortRef):
         >>> A.range()
         Bool
         """
-        return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)
+        return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)    
 
 class ArrayRef(ExprRef):
     """Array expressions. """
@@ -4162,6 +4162,16 @@ def Select(a, i):
         _z3_assert(is_array(a), "First argument must be a Z3 array expression")
     return a[i]
 
+def Default(a):
+    """ Return a default value for array expression.
+    >>> b = K(IntSort(), 1)
+    >>> prove(Default(b) == 1)
+    proved
+    """
+    if __debug__:
+        _z3_assert(is_array(a), "First argument must be a Z3 array expression")
+    return a.mk_default()
+    
 def Map(f, *args):
     """Return a Z3 map array expression.
 
diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 22751aa46..546f037de 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -664,3 +664,45 @@ algebraic_numbers::anum const & arith_util::to_irrational_algebraic_numeral(expr
     SASSERT(is_irrational_algebraic_numeral(n));
     return plugin().aw().to_anum(to_app(n)->get_decl());
 }
+
+expr_ref arith_util::mk_mul_simplify(expr_ref_vector const& args) {
+    return mk_mul_simplify(args.size(), args.c_ptr());
+
+}
+expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) {
+    expr_ref result(m_manager);
+    
+    switch (sz) {
+    case 0:
+        result = mk_numeral(rational(1), true);
+        break;
+    case 1:
+        result = args[0];
+        break;
+    default:
+        result = mk_mul(sz, args);
+        break;                    
+    }
+    return result;
+}
+
+expr_ref arith_util::mk_add_simplify(expr_ref_vector const& args) {
+    return mk_add_simplify(args.size(), args.c_ptr());
+
+}
+expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
+    expr_ref result(m_manager);
+    
+    switch (sz) {
+    case 0:
+        result = mk_numeral(rational(0), true);
+        break;
+    case 1:
+        result = args[0];
+        break;
+    default:
+        result = mk_add(sz, args);
+        break;                    
+    }
+    return result;
+}
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 25356a667..b72a55e34 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -149,7 +149,6 @@ protected:
     func_decl * m_mod_0_decl;
     func_decl * m_u_asin_decl;
     func_decl * m_u_acos_decl;
-
     ptr_vector<app> m_small_ints;
     ptr_vector<app> m_small_reals;
 
@@ -416,6 +415,11 @@ public:
         return m_manager.mk_eq(lhs, rhs);
     }
 
+    expr_ref mk_mul_simplify(expr_ref_vector const& args);
+    expr_ref mk_mul_simplify(unsigned sz, expr* const* args);
+
+    expr_ref mk_add_simplify(expr_ref_vector const& args);
+    expr_ref mk_add_simplify(unsigned sz, expr* const* args);
 };
 
 #endif /* ARITH_DECL_PLUGIN_H_ */
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 7d5248b30..1afa13117 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -1200,6 +1200,14 @@ std::ostream& operator<<(std::ostream& out, app_ref const&  e) {
     return out << mk_ismt2_pp(e.get(), e.get_manager());
 }
 
+std::ostream& operator<<(std::ostream& out, func_decl_ref const&  e) {
+    return out << mk_ismt2_pp(e.get(), e.get_manager());
+}
+
+std::ostream& operator<<(std::ostream& out, sort_ref const&  e) {
+    return out << mk_ismt2_pp(e.get(), e.get_manager());
+}
+
 std::ostream& operator<<(std::ostream& out, expr_ref_vector const&  e) {
     for (unsigned i = 0; i < e.size(); ++i) {
         out << mk_ismt2_pp(e[i], e.get_manager());
@@ -1216,6 +1224,18 @@ std::ostream& operator<<(std::ostream& out, app_ref_vector const&  e) {
     return out;
 }
 
+std::ostream& operator<<(std::ostream& out, func_decl_ref_vector const&  e) {
+    for (unsigned i = 0; i < e.size(); ++i) 
+        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    return out;
+}
+
+std::ostream& operator<<(std::ostream& out, sort_ref_vector const&  e) {
+    for (unsigned i = 0; i < e.size(); ++i) 
+        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    return out;
+}
+
 #ifdef Z3DEBUG
 void pp(expr const * n, ast_manager & m) {
     std::cout << mk_ismt2_pp(const_cast<expr*>(n), m) << std::endl;
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 45d18ceff..f2d177041 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -117,8 +117,13 @@ std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p);
 
 std::ostream& operator<<(std::ostream& out, expr_ref const& e);
 std::ostream& operator<<(std::ostream& out, app_ref const& e);
+std::ostream& operator<<(std::ostream& out, func_decl_ref const& e);
+std::ostream& operator<<(std::ostream& out, sort_ref const& e);
+
 
 std::ostream& operator<<(std::ostream& out, expr_ref_vector const& e);
 std::ostream& operator<<(std::ostream& out, app_ref_vector const& e);
+std::ostream& operator<<(std::ostream& out, func_decl_ref_vector const& e);
+std::ostream& operator<<(std::ostream& out, sort_ref_vector const& e);
 
 #endif
diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp
index eba4d526b..0129a88d5 100644
--- a/src/ast/ast_util.cpp
+++ b/src/ast/ast_util.cpp
@@ -170,7 +170,6 @@ app* mk_and(ast_manager & m, unsigned num_args, app * const * args) {
     return to_app(mk_and(m, num_args, (expr* const*) args));
 }
 
-
 expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
     if (num_args == 0)
         return m.mk_false();
@@ -188,10 +187,43 @@ expr * mk_not(ast_manager & m, expr * arg) {
     expr * atom;
     if (m.is_not(arg, atom))
         return atom;
+    else if (m.is_true(arg)) 
+        return m.mk_false();
+    else if (m.is_false(arg))
+        return m.mk_true();
     else
         return m.mk_not(arg);
 }
 
+expr_ref push_not(const expr_ref& e) {
+    ast_manager& m = e.get_manager();
+    if (!is_app(e)) {
+        return expr_ref(m.mk_not(e), m);
+    }
+    app* a = to_app(e);
+    if (m.is_and(a)) {
+        if (a->get_num_args() == 0) {
+            return expr_ref(m.mk_false(), m);
+        }
+        expr_ref_vector args(m);
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            args.push_back(push_not(expr_ref(a->get_arg(i), m)));
+        }
+        return mk_or(args);
+    }
+    if (m.is_or(a)) {
+        if (a->get_num_args() == 0) {
+            return expr_ref(m.mk_true(), m);
+        }
+        expr_ref_vector args(m);
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            args.push_back(push_not(expr_ref(a->get_arg(i), m)));
+        }
+        return mk_and(args);
+    }
+    return expr_ref(mk_not(m, e), m);    
+}
+
 expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args) {
     expr_ref_buffer new_diseqs(m);
     for (unsigned i = 0; i < num_args; i++) {
@@ -201,6 +233,24 @@ expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args)
     return mk_and(m, new_diseqs.size(), new_diseqs.c_ptr());
 }
 
+expr* mk_distinct(ast_manager& m, unsigned num_args, expr * const * args) {
+    switch (num_args) {
+    case 0:
+    case 1:
+        return m.mk_true();
+    case 2:
+        return m.mk_not(m.mk_eq(args[0], args[1]));
+    default:
+        return m.mk_distinct(num_args, args);
+    }
+}
+
+expr_ref mk_distinct(expr_ref_vector const& args) {
+    ast_manager& m = args.get_manager();
+    return expr_ref(mk_distinct(m, args.size(), args.c_ptr()), m);
+}
+
+
 void flatten_and(expr_ref_vector& result) {
     ast_manager& m = result.get_manager();
     expr* e1, *e2, *e3;
diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h
index 311001a19..6244e16b9 100644
--- a/src/ast/ast_util.h
+++ b/src/ast/ast_util.h
@@ -121,18 +121,29 @@ app  * mk_or(ast_manager & m, unsigned num_args, app * const * args);
 inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 
-
 /**
    Return a          if arg = (not a)
    Retur (not arg)   otherwise
  */
 expr * mk_not(ast_manager & m, expr * arg);
 
+/**
+   Negate and push over conjunction or disjunction.
+ */
+expr_ref push_not(const expr_ref& arg);
+
 /**
    Return the expression (and (not (= args[0] args[1])) (not (= args[0] args[2])) ... (not (= args[num_args-2] args[num_args-1])))
 */
 expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args);
 
+/**
+   Create simplified distinct term. Binary distinct becomes a single disequality.
+ */
+expr * mk_distinct(ast_manager& m, unsigned num_args, expr * const * args);
+
+expr_ref mk_distinct(expr_ref_vector const& args);
+
 /**
    \brief Collect top-level conjunctions and disjunctions.
 */
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index f65462d1b..b1f3491fe 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -865,6 +865,12 @@ sort * bv_util::mk_sort(unsigned bv_size) {
     return m_manager.mk_sort(get_fid(), BV_SORT, 1, p);
 }
 
+unsigned bv_util::get_int2bv_size(parameter const& p) {
+    int sz;
+    VERIFY(m_plugin->get_int2bv_size(1, &p, sz));
+    return static_cast<unsigned>(sz);
+}
+
 app * bv_util::mk_bv2int(expr* e) {
     sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT);
     parameter p(s);
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index 563622338..ac0ff7f79 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -234,7 +234,6 @@ protected:
 
     func_decl * mk_mkbv(unsigned arity, sort * const * domain);
 
-    bool get_int2bv_size(unsigned num_parameters, parameter const * parameters, int & result);
 
     func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity);
 
@@ -267,6 +266,8 @@ public:
 
     virtual expr * get_some_value(sort * s);
 
+    bool get_int2bv_size(unsigned num_parameters, parameter const * parameters, int & result);
+
     virtual bool is_considered_uninterpreted(func_decl * f) {
         if (f->get_family_id() != get_family_id())
             return false;
@@ -390,6 +391,8 @@ public:
         return static_cast<unsigned>(s->get_parameter(0).get_int());
     }
     unsigned get_bv_size(expr const * n) const { return get_bv_size(m_manager.get_sort(n)); }
+    unsigned get_int2bv_size(parameter const& p);
+
 
     app * mk_ule(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_ULEQ, arg1, arg2); }
     app * mk_sle(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLEQ, arg1, arg2); }
@@ -427,6 +430,7 @@ public:
     app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); }
 
     app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); }
+
 };
 
 #endif /* BV_DECL_PLUGIN_H_ */
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index c185540b7..d837ebb22 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -1000,3 +1000,25 @@ void datatype_util::display_datatype(sort *s0, std::ostream& strm) {
     }
 
 }
+
+bool datatype_util::is_func_decl(datatype_op_kind k, unsigned num_params, parameter const* params, func_decl* f) {
+    bool eq = 
+        f->get_decl_kind() == k &&
+        f->get_family_id() == m_family_id &&
+        f->get_num_parameters() == num_params;
+    for (unsigned i = 0; eq && i < num_params; ++i) {
+        eq = params[i] == f->get_parameter(i);
+    }
+    return eq;
+}
+
+bool datatype_util::is_constructor_of(unsigned num_params, parameter const* params, func_decl* f) {
+    return 
+        num_params == 2 &&
+        m_family_id == f->get_family_id() &&
+        OP_DT_CONSTRUCTOR == f->get_decl_kind() &&
+        2 == f->get_num_parameters() &&
+        params[0] == f->get_parameter(0) &&
+        params[1] == f->get_parameter(1);
+}
+
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 99be75493..51d33c896 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -209,6 +209,8 @@ public:
     func_decl * get_recognizer_constructor(func_decl * recognizer);
     family_id get_family_id() const { return m_family_id; }
     bool are_siblings(sort * s1, sort * s2);
+    bool is_func_decl(datatype_op_kind k, unsigned num_params, parameter const* params, func_decl* f);
+    bool is_constructor_of(unsigned num_params, parameter const* params, func_decl* f);
     void reset();
     void display_datatype(sort *s, std::ostream& strm);
 
diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp
index 949168cad..513162043 100644
--- a/src/ast/expr_abstract.cpp
+++ b/src/ast/expr_abstract.cpp
@@ -22,6 +22,10 @@ Notes:
 
 void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
     
+    if (num_bound == 0) {
+        result = n;
+        return;
+    }
     expr * curr = 0, *b = 0;
     SASSERT(n->get_ref_count() > 0);
 
@@ -106,3 +110,27 @@ void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* cons
     expr_abstractor abs(m);
     abs(base, num_bound, bound, n, result);
 }
+
+expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
+    expr_ref result(m);
+    expr_abstract(m, 0, num_bound, (expr* const*)bound, n, result);    
+    if (num_bound > 0) {
+        ptr_vector<sort> sorts;
+        svector<symbol> names;
+        for (unsigned i = 0; i < num_bound; ++i) {
+            sorts.push_back(m.get_sort(bound[i]));
+            names.push_back(bound[i]->get_decl()->get_name());
+        }
+        result = m.mk_quantifier(is_forall, num_bound, sorts.c_ptr(), names.c_ptr(), result);
+    }
+    return result;
+
+}
+
+expr_ref mk_forall(ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
+    return mk_quantifier(true, m, num_bound, bound, n);
+}
+
+expr_ref mk_exists(ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
+    return mk_quantifier(false, m, num_bound, bound, n);
+}
diff --git a/src/ast/expr_abstract.h b/src/ast/expr_abstract.h
index 7f43ecf83..5c91a914e 100644
--- a/src/ast/expr_abstract.h
+++ b/src/ast/expr_abstract.h
@@ -33,6 +33,8 @@ public:
 };
 
 void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref&  result);
+expr_ref mk_forall(ast_manager& m, unsigned num_bound, app* const* bound, expr* n);
+expr_ref mk_exists(ast_manager& m, unsigned num_bound, app* const* bound, expr* n);
 
 #endif
 
diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp
index 25a8fd657..2655ac00d 100644
--- a/src/ast/rewriter/expr_safe_replace.cpp
+++ b/src/ast/rewriter/expr_safe_replace.cpp
@@ -30,6 +30,14 @@ void expr_safe_replace::insert(expr* src, expr* dst) {
     m_subst.insert(src, dst);
 }
 
+void expr_safe_replace::operator()(expr_ref_vector& es) {
+    expr_ref val(m);
+    for (unsigned i = 0; i < es.size(); ++i) {
+        (*this)(es[i].get(), val);
+        es[i] = val;
+    }
+}
+
 void expr_safe_replace::operator()(expr* e, expr_ref& res) {
     m_todo.push_back(e);
     expr* a, *b;
diff --git a/src/ast/rewriter/expr_safe_replace.h b/src/ast/rewriter/expr_safe_replace.h
index fe7033439..84a74ccaa 100644
--- a/src/ast/rewriter/expr_safe_replace.h
+++ b/src/ast/rewriter/expr_safe_replace.h
@@ -42,6 +42,8 @@ public:
 
     void operator()(expr* src, expr_ref& e);
 
+    void operator()(expr_ref_vector& es);
+
     void apply_substitution(expr* s, expr* def, expr_ref& t);
 
     void reset();
diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp
index dd9062828..e59a079e7 100644
--- a/src/ast/rewriter/quant_hoist.cpp
+++ b/src/ast/rewriter/quant_hoist.cpp
@@ -73,7 +73,7 @@ public:
         unsigned nd = q->get_num_decls();
         for (unsigned i = 0; i < nd; ++i) {
             sort* s = q->get_decl_sort(i);
-            app* a = m.mk_fresh_const("x", s);
+            app* a = m.mk_fresh_const(q->get_decl_name(i).str().c_str(), s);
             vars.push_back(a);
         }
         expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd);
@@ -154,9 +154,7 @@ private:
     }
     
     quantifier_type& negate(quantifier_type& qt) {
-        TRACE("qe", display(qt, tout); tout << "\n";);
         qt = static_cast<quantifier_type>(qt ^0x1);
-        TRACE("qe", display(qt, tout); tout << "\n";);
         return qt;
     }
     
@@ -205,6 +203,7 @@ private:
         case AST_APP: {
             expr_ref_vector args(m);
             expr_ref tmp(m);
+            expr* t1, *t2, *t3;
             unsigned num_args = 0;
             app* a = to_app(fml);
             if (m.is_and(fml)) {
@@ -228,16 +227,35 @@ private:
                 negate(qt);
                 result = m.mk_not(tmp);
             }
-            else if (m.is_implies(fml)) {
-                pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
+            else if (m.is_implies(fml, t1, t2)) {
+                pull_quantifier(t1, negate(qt), vars, tmp);
                 negate(qt);
-                pull_quantifier(to_app(fml)->get_arg(1), qt, vars, result);
+                pull_quantifier(t2, qt, vars, result);
                 result = m.mk_implies(tmp, result);
             }
-            else if (m.is_ite(fml)) {
-                pull_quantifier(to_app(fml)->get_arg(1), qt, vars, tmp);
-                pull_quantifier(to_app(fml)->get_arg(2), qt, vars, result);
-                result = m.mk_ite(to_app(fml)->get_arg(0), tmp, result);
+            else if (m.is_ite(fml, t1, t2, t3)) {
+                expr_ref tt1(m), tt2(m), tt3(m), ntt1(m), nt1(m);
+                pull_quantifier(t2, qt, vars, tt2);
+                pull_quantifier(t3, qt, vars, tt3);
+                if (has_quantifiers(t1)) {
+                    pull_quantifier(t1, qt, vars, tt1);
+                    nt1 = m.mk_not(t1);
+                    pull_quantifier(nt1, qt, vars, ntt1);
+                    result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3));
+                }
+                else {
+                    result = m.mk_ite(t1, tt2, tt3);
+                }
+            }
+            else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) {
+                expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m);
+                pull_quantifier(t1, qt, vars, tt1);
+                pull_quantifier(t2, qt, vars, tt2);
+                nt1 = m.mk_not(t1);
+                nt2 = m.mk_not(t2);
+                pull_quantifier(nt1, qt, vars, ntt1);
+                pull_quantifier(nt2, qt, vars, ntt2);
+                result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1));
             }
             else {
                 // the formula contains a quantifier, but it is "inaccessible"
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 1c5da3829..f044c9736 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -303,8 +303,8 @@ public:
             goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
             assert_exprs_from(ctx, *g);
 
-            unsigned timeout   = p.get_uint("timeout", UINT_MAX);
-            unsigned rlimit  =   p.get_uint("rlimit", 0);
+            unsigned timeout   = p.get_uint("timeout", ctx.params().m_timeout);
+            unsigned rlimit  =   p.get_uint("rlimit", ctx.params().m_rlimit);
 
             goal_ref_buffer     result_goals;
             model_converter_ref mc;
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index e00c1f29f..f4eb8a003 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -539,7 +539,6 @@ namespace algebraic_numbers {
         }
 
         bool factor(scoped_upoly const & up, factors & r) {
-            // std::cout << "factor: "; upm().display(std::cout, up); std::cout << std::endl;
             if (m_factor) {
                 return upm().factor(up, r, m_factor_params);
             }
@@ -547,7 +546,7 @@ namespace algebraic_numbers {
                 scoped_upoly & up_sqf = m_isolate_tmp3;
                 up_sqf.reset();
                 upm().square_free(up.size(), up.c_ptr(), up_sqf);
-                TRACE("anum_bug", upm().display(tout, up_sqf.size(), up_sqf.c_ptr()); tout << "\n";);
+                TRACE("algebraic", upm().display(tout, up_sqf.size(), up_sqf.c_ptr()); tout << "\n";);
                 r.push_back(up_sqf, 1);
                 return false;
             }
@@ -566,6 +565,7 @@ namespace algebraic_numbers {
         }
 
         void isolate_roots(scoped_upoly const & up, numeral_vector & roots) {
+            TRACE("algebraic", upm().display(tout, up); tout << "\n";);
             if (up.empty())
                 return; // ignore the zero polynomial
             factors & fs = m_isolate_factors;
@@ -586,6 +586,7 @@ namespace algebraic_numbers {
                 upolynomial::numeral_vector const & f = fs[i];
                 // polynomial f contains the non zero roots
                 unsigned d = upm().degree(f);
+                TRACE("algebraic", tout << "factor " << i << " degree: " << d << "\n";);
                 if (d == 0)
                     continue; // found all roots of f
                 scoped_mpq r(qm());
@@ -601,8 +602,9 @@ namespace algebraic_numbers {
                 }
                 SASSERT(m_isolate_roots.empty() && m_isolate_lowers.empty() && m_isolate_uppers.empty());
                 upm().sqf_isolate_roots(f.size(), f.c_ptr(), bqm(), m_isolate_roots, m_isolate_lowers, m_isolate_uppers);
-                // collect rational/basic roots
+                // collect rational/basic roots                
                 unsigned sz = m_isolate_roots.size();
+                TRACE("algebraic", tout << "isolated roots: " << sz << "\n";);
                 for (unsigned i = 0; i < sz; i++) {
                     to_mpq(qm(), m_isolate_roots[i], r);
                     roots.push_back(numeral(mk_basic_cell(r)));
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index 8b4344ce6..f20a77bda 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -29,7 +29,6 @@ Revision History:
 #include"ast_counter.h"
 #include"statistics.h"
 #include"lbool.h"
-#include"qe_util.h"
 
 namespace datalog {
 
diff --git a/src/muz/pdr/pdr_closure.cpp b/src/muz/pdr/pdr_closure.cpp
index eacbb0b28..746b12416 100644
--- a/src/muz/pdr/pdr_closure.cpp
+++ b/src/muz/pdr/pdr_closure.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include "pdr_closure.h"
 #include "pdr_context.h"
 #include "expr_safe_replace.h"
+#include "ast_util.h"
 
 namespace pdr {
 
@@ -147,7 +148,7 @@ namespace pdr {
         for (unsigned i = 0; i < fmls.size(); ++i) {
             fmls[i] = close_fml(fmls[i].get());            
         }
-        return qe::mk_and(fmls);
+        return expr_ref(mk_and(fmls), m);
     }
 
     expr_ref closure::relax(unsigned i, expr* fml) {
@@ -169,7 +170,7 @@ namespace pdr {
         for (unsigned i = 0; i < As.size(); ++i) {
             fmls.push_back(relax(i, As[i]));
         }
-        B = qe::mk_and(fmls);
+        B = mk_and(fmls);
         return B;
     }
 
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index bd7ce0b3c..1c25b015d 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -45,7 +45,6 @@ Notes:
 #include "smt_value_sort.h"
 #include "proof_utils.h"
 #include "dl_boogie_proof.h"
-#include "qe_util.h"
 #include "scoped_proof.h"
 #include "blast_term_ite_tactic.h"
 #include "model_implicant.h"
diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp
index 94265e95d..0565cb23b 100644
--- a/src/muz/pdr/pdr_farkas_learner.cpp
+++ b/src/muz/pdr/pdr_farkas_learner.cpp
@@ -201,7 +201,7 @@ namespace pdr {
                 lits.push_back(extract_consequence(lo, hi));
                 lo = hi;
             }
-            res = qe::mk_or(lits);
+            res = mk_or(lits);
             IF_VERBOSE(2, { if (lits.size() > 1) { verbose_stream() << "combined lemma: " << mk_pp(res, m) << "\n"; } });
 #endif
         }
@@ -415,6 +415,7 @@ namespace pdr {
                 return false;
             }
         }
+
     };
 
     class collect_pure_proc {
diff --git a/src/muz/pdr/pdr_generalizers.cpp b/src/muz/pdr/pdr_generalizers.cpp
index fd700cfd7..5b7e11877 100644
--- a/src/muz/pdr/pdr_generalizers.cpp
+++ b/src/muz/pdr/pdr_generalizers.cpp
@@ -117,7 +117,7 @@ namespace pdr {
     void core_farkas_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
         ast_manager& m  = n.pt().get_manager();
         if (core.empty()) return;
-        expr_ref A(m), B(qe::mk_and(core)), C(m);
+        expr_ref A(m), B(mk_and(core)), C(m);
         expr_ref_vector Bs(m);
         flatten_or(B, Bs);
         A = n.pt().get_propagation_formula(m_ctx.get_pred_transformers(), n.level());
@@ -129,13 +129,13 @@ namespace pdr {
             if (m_farkas_learner.get_lemma_guesses(A, B, lemmas)) {
                 TRACE("pdr", 
                       tout << "Old core:\n" << mk_pp(B, m) << "\n";
-                      tout << "New core:\n" << mk_pp(qe::mk_and(lemmas), m) << "\n";);            
-                Bs[i] = qe::mk_and(lemmas);
+                      tout << "New core:\n" << mk_and(lemmas) << "\n";);            
+                Bs[i] = mk_and(lemmas);
                 change = true;
             }
         }
         if (change) {
-            C = qe::mk_or(Bs);
+            C = mk_or(Bs);
             TRACE("pdr", tout << "prop:\n" << mk_pp(A,m) << "\ngen:" << mk_pp(B, m) << "\nto: " << mk_pp(C, m) << "\n";);
             core.reset();
             flatten_and(C, core);    
@@ -186,7 +186,7 @@ namespace pdr {
         }        
         closure cl(n.pt(), m_is_closure);
 
-        expr_ref fml1 = qe::mk_and(core);        
+        expr_ref fml1 = mk_and(core);        
         expr_ref fml2 = n.pt().get_formulas(n.level(), false);
         fml1_2.push_back(fml1);
         fml1_2.push_back(0);
@@ -205,7 +205,7 @@ namespace pdr {
             if (l_false == n.pt().is_reachable(nd, &conv2, uses_level1)) {
                 new_cores.push_back(std::make_pair(conv2, uses_level1));
                 change = true;
-                expr_ref state1 = qe::mk_and(conv2);
+                expr_ref state1 = mk_and(conv2);
                 TRACE("pdr", 
                       tout << mk_pp(state, m) << "\n";
                       tout << "Generalized to:\n" << mk_pp(state1, m) << "\n";);
@@ -593,7 +593,7 @@ namespace pdr {
             for (unsigned i = ut_size; i < t_size; i++) {
                 conj.push_back(rule.get_tail(i));
             }         
-            result = qe::mk_and(conj);
+            result = mk_and(conj);
             if (!sub.empty()) {
                 expr_ref tmp = result;
                 var_subst(m, false)(tmp, sub.size(), sub.c_ptr(), result);
@@ -685,7 +685,7 @@ namespace pdr {
             for (unsigned i = 0; i < rules.size(); ++i) {
                 fmls.push_back(m.mk_not(mk_transition_rule(reps, level, *rules[i])));           
             }
-            fml = qe::mk_and(fmls);
+            fml = mk_and(fmls);
             TRACE("pdr", tout << mk_pp(fml, m) << "\n";);
             return fml;
         }
@@ -741,7 +741,7 @@ namespace pdr {
                 }                
             }
 
-            expr_ref result = qe::mk_and(conjs);
+            expr_ref result = mk_and(conjs);
             TRACE("pdr", tout << mk_pp(result, m) << "\n";);
             return result;
         }
diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp
index 7c6dac5e4..e630d7083 100644
--- a/src/muz/rel/check_relation.cpp
+++ b/src/muz/rel/check_relation.cpp
@@ -6,7 +6,6 @@ Copyright (c) 2015 Microsoft Corporation
 
 #include "check_relation.h"
 #include "dl_relation_manager.h"
-#include "qe_util.h"
 #include "ast_util.h"
 #include "smt_kernel.h"
 #include <typeinfo>
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 140d1e94d..dda674131 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -23,7 +23,6 @@ Notes:
 --*/
 #include "udoc_relation.h"
 #include "dl_relation_manager.h"
-#include "qe_util.h"
 #include "ast_util.h"
 #include "smt_kernel.h"
 
diff --git a/src/nlsat/nlsat_assignment.h b/src/nlsat/nlsat_assignment.h
index 178a7f738..a52a84f3b 100644
--- a/src/nlsat/nlsat_assignment.h
+++ b/src/nlsat/nlsat_assignment.h
@@ -39,6 +39,17 @@ namespace nlsat {
             m_values.swap(other.m_values);
             m_assigned.swap(other.m_assigned);
         }
+        void copy(assignment const& other) {
+            m_assigned.reset();
+            m_assigned.append(other.m_assigned);
+            m_values.reserve(m_assigned.size(), anum());
+            for (unsigned i = 0; i < m_assigned.size(); ++i) {
+                if (is_assigned(i)) {
+                    am().set(m_values[i], other.value(i));
+                }
+            }
+        }
+
         void set_core(var x, anum & v) {
             m_values.reserve(x+1, anum());
             m_assigned.reserve(x+1, false); 
@@ -52,11 +63,26 @@ namespace nlsat {
             am().set(m_values[x], v); 
         }
         void reset(var x) { if (x < m_assigned.size()) m_assigned[x] = false; }
+        void reset() { m_assigned.reset(); }
         bool is_assigned(var x) const { return m_assigned.get(x, false); }
         anum const & value(var x) const { return m_values[x]; }
         virtual anum_manager & m() const { return am(); }
         virtual bool contains(var x) const { return is_assigned(x); }
         virtual anum const & operator()(var x) const { SASSERT(is_assigned(x)); return value(x); }
+        void swap(var x, var y) {
+            SASSERT(x < m_values.size() && y < m_values.size());
+            std::swap(m_assigned[x], m_assigned[y]);
+            std::swap(m_values[x], m_values[y]);
+        }
+        void display(std::ostream& out) const {
+            for (unsigned i = 0; i < m_assigned.size(); ++i) {
+                if (m_assigned[i]) {
+                    out << "x" << i << " := ";
+                    m_values.m().display(out, m_values[i]);
+                    out << "\n";
+                }
+            }
+        }
     };
     
     /**
diff --git a/src/nlsat/nlsat_types.h b/src/nlsat/nlsat_types.h
index e6ab30c19..dcc68d8e1 100644
--- a/src/nlsat/nlsat_types.h
+++ b/src/nlsat/nlsat_types.h
@@ -111,6 +111,20 @@ namespace nlsat {
         struct eq_proc { bool operator()(ineq_atom const * a1, ineq_atom const * a2) const; };
     };
 
+    inline std::ostream& operator<<(std::ostream& out, atom::kind k) {
+        switch (k) {
+        case atom::kind::EQ: return out << "=";
+        case atom::kind::LT: return out << "<";
+        case atom::kind::ROOT_EQ: return out << "= root";
+        case atom::kind::ROOT_LT: return out << "< root";
+        case atom::kind::ROOT_LE: return out << "<= root";
+        case atom::kind::ROOT_GT: return out << "> root";
+        case atom::kind::ROOT_GE: return out << ">= root";
+        default: UNREACHABLE();
+        }
+        return out;
+    }
+
     class root_atom : public atom {
         friend class solver;
         var      m_x;
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index 085cb4de3..1399d6549 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -60,7 +60,7 @@ class nla2bv_tactic : public tactic {
         expr_ref_vector             m_trail;
         unsigned                    m_num_bits;
         unsigned                    m_default_bv_size;
-        ref<filter_model_converter> m_fmc;
+        filter_model_converter_ref  m_fmc;
         
     public:
         imp(ast_manager & m, params_ref const& p):
diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index 25127cb90..c010ed0af 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -60,7 +60,7 @@ struct bv_size_reduction_tactic::imp {
     obj_map<app, numeral>     m_unsigned_lowers;
     obj_map<app, numeral>     m_unsigned_uppers;
     ref<bv_size_reduction_mc> m_mc;
-    ref<filter_model_converter> m_fmc;
+    filter_model_converter_ref m_fmc;
     scoped_ptr<expr_replacer> m_replacer;
     bool                      m_produce_models;
 
diff --git a/src/util/obj_pair_set.h b/src/util/obj_pair_set.h
index 4c8ed698a..29139a51d 100644
--- a/src/util/obj_pair_set.h
+++ b/src/util/obj_pair_set.h
@@ -45,6 +45,7 @@ public:
     bool contains(T1 * t1, T2 * t2) const { return m_set.contains(obj_pair(t1, t2)); }
     bool contains(obj_pair const & p) const { return m_set.contains(p); }
     void reset() { m_set.reset(); }
+    bool empty() const { return m_set.empty(); }
 };
 
 #endif
diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp
index 6ad1af112..aee84c1f0 100644
--- a/src/util/small_object_allocator.cpp
+++ b/src/util/small_object_allocator.cpp
@@ -69,6 +69,7 @@ void small_object_allocator::reset() {
 #define MASK ((1 << PTR_ALIGNMENT) - 1)
 
 void small_object_allocator::deallocate(size_t size, void * p) {
+    if (size == 0) return;
 #if defined(Z3DEBUG) && !defined(_WINDOWS)
     // Valgrind friendly
     memory::deallocate(p);
@@ -91,6 +92,7 @@ void small_object_allocator::deallocate(size_t size, void * p) {
 }
 
 void * small_object_allocator::allocate(size_t size) {
+    if (size == 0) return 0;
 #if defined(Z3DEBUG) && !defined(_WINDOWS)
     // Valgrind friendly
     return memory::allocate(size);