diff --git a/scripts/update_api.py b/scripts/update_api.py
index 2828a63f8..45ea9be23 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -240,7 +240,7 @@ def param2javaw(p):
     if k == OUT:
         return "jobject"
     elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
-        if param_type(p) == INT or param_type(p) == UINT:
+        if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
             return "jintArray"
         else:
             return "jlongArray"
@@ -258,7 +258,7 @@ def param2pystr(p):
 def param2ml(p):
     k = param_kind(p)
     if k == OUT:
-        if param_type(p) == INT or param_type(p) == UINT or param_type(p) == INT64 or param_type(p) == UINT64:
+        if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL or param_type(p) == INT64 or param_type(p) == UINT64:
             return "int"
         elif param_type(p) == STRING:
             return "string"
@@ -491,7 +491,7 @@ def java_method_name(name):
 
 # Return the type of the java array elements
 def java_array_element_type(p):
-    if param_type(p) == INT or param_type(p) == UINT:
+    if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
         return 'jint'
     else:
         return 'jlong'
@@ -653,7 +653,7 @@ def mk_java(java_dir, package_name):
             if k == OUT or k == INOUT:
                 java_wrapper.write('  %s _a%s;\n' % (type2str(param_type(param)), i))
             elif k == IN_ARRAY or k == INOUT_ARRAY:
-                if param_type(param) == INT or param_type(param) == UINT:
+                if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
                     java_wrapper.write('  %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i))
                 else:
                     java_wrapper.write('  GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i))
@@ -663,7 +663,7 @@ def mk_java(java_dir, package_name):
                                                                                                      type2str(param_type(param)),
                                                                                                      param_array_capacity_pos(param),
                                                                                                      type2str(param_type(param))))
-                if param_type(param) == INT or param_type(param) == UINT:
+                if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
                     java_wrapper.write('  jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
                 else:
                     java_wrapper.write('  GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
@@ -702,19 +702,19 @@ def mk_java(java_dir, package_name):
         for param in params:
             k = param_kind(param)
             if k == OUT_ARRAY:
-                if param_type(param) == INT or param_type(param) == UINT:
+                if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
                     java_wrapper.write('  jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
                 else:
                     java_wrapper.write('  SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i))
                 java_wrapper.write('  free(_a%s);\n' % i)
             elif k == IN_ARRAY or k == OUT_ARRAY:
-                if param_type(param) == INT or param_type(param) == UINT:
+                if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
                     java_wrapper.write('  jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i))
                 else:
                     java_wrapper.write('  RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i))
 
             elif k == OUT or k == INOUT:
-                if param_type(param) == INT or param_type(param) == UINT:
+                if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
                     java_wrapper.write('  {\n')
                     java_wrapper.write('     jclass mc    = jenv->GetObjectClass(a%s);\n' % i)
                     java_wrapper.write('     jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
@@ -957,7 +957,7 @@ def def_API(name, result, params):
                 log_c.write(" }\n")
                 log_c.write("  Au(a%s);\n" % sz)
                 exe_c.write("in.get_uint_array(%s)" % i)
-            elif ty == INT:
+            elif ty == INT or ty == BOOL:
                 log_c.write("U(a%s[i]);" % i)
                 log_c.write(" }\n")
                 log_c.write("  Au(a%s);\n" % sz)
diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index 95bc0bef9..9a778d6e0 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -387,4 +387,17 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_FALSE);
     }
 
+    Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits) {
+        Z3_TRY;
+        LOG_Z3_mk_bv_numeral(c, sz, bits);
+        RESET_ERROR_CODE();
+        rational r(0);
+        for (unsigned i = 0; i < sz; ++i) {
+            if (bits[i]) r += rational::power_of_two(i);
+        }
+        ast * a = mk_c(c)->mk_numeral_core(r, mk_c(c)->bvutil().mk_sort(sz));
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(0);
+    }
+
 };
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 23a7bd22e..4b5e9d04e 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -301,6 +301,7 @@ namespace z3 {
         expr bv_val(__int64 n, unsigned sz);
         expr bv_val(__uint64 n, unsigned sz);
         expr bv_val(char const * n, unsigned sz);
+        expr bv_val(unsigned n, bool const* bits);
 
         expr string_val(char const* s);
         expr string_val(std::string const& s);
@@ -964,6 +965,13 @@ namespace z3 {
         friend expr operator|(expr const & a, expr const & b);
         friend expr operator|(expr const & a, int b);
         friend expr operator|(int a, expr const & b);
+        friend expr nand(expr const& a, expr const& b);
+        friend expr nor(expr const& a, expr const& b);
+        friend expr xnor(expr const& a, expr const& b);
+
+        expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
+        expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
+        expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
 
         friend expr operator~(expr const & a);
         expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }        
@@ -1332,6 +1340,10 @@ namespace z3 {
     inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
     inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
 
+    inline expr nand(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr nor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr xnor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
+
     inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
 
 
@@ -1406,11 +1418,18 @@ namespace z3 {
     inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
 
     /**
-       \brief signed reminder operator for bitvectors
+       \brief signed remainder operator for bitvectors
     */
     inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
     inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
     inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
+
+    /**
+       \brief signed modulus operator for bitvectors
+    */
+    inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
+    inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
+    inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
     
     /**
        \brief unsigned reminder operator for bitvectors
@@ -2455,6 +2474,11 @@ namespace z3 {
     inline expr context::bv_val(__int64 n, unsigned sz) { Z3_ast r = Z3_mk_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
     inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
     inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
+    inline expr context::bv_val(unsigned n, bool const* bits) { 
+        array<Z3_bool> _bits(n);
+        for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
+        Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r); 
+    }
 
     inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
     inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 27711be81..914cee615 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3127,6 +3127,20 @@ namespace Microsoft.Z3
 
             return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
         }
+
+        /// <summary>
+        /// Create a bit-vector numeral.
+        /// </summary>
+        /// <param name="bits">An array of bits representing the bit-vector. Least signficant bit is at position 0.</param>
+        public BitVecNum MkBV(bool[] bits)
+        {
+            Contract.Ensures(Contract.Result<BitVecNum>() != null);
+            int[] _bits = new int[bits.Length];
+            for (int i = 0; i < bits.Length; ++i) _bits[i] = bits[i] ? 1 : 0;	
+            return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
+        }
+
+
         #endregion
 
         #endregion // Numerals
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 9f155b45e..cf1c8fca7 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -3248,6 +3248,14 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, __uint64 v, Z3_sort ty);
 
+    /**
+       \brief create a bit-vector numeral from a vector of Booleans.
+       
+       \sa Z3_mk_numeral
+       def_API('Z3_mk_bv_numeral', AST, (_in(CONTEXT), _in(UINT), _in_array(1, BOOL)))
+    */
+    Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits);
+
     /*@}*/
 
     /** @name Sequences and regular expressions */
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 98c1bdfed..e7d808b2b 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1684,22 +1684,9 @@ ast * ast_manager::register_node_core(ast * n) {
     CASSERT("nondet_bug", contains || slow_not_contains(n));
 #endif
     
-#if 0
-    static unsigned counter = 0;
-    counter++;
-    if (counter % 100000 == 0)
-        verbose_stream() << "[ast-table] counter: " << counter << " collisions: " << m_ast_table.collisions() << " capacity: " << m_ast_table.capacity() << " size: " << m_ast_table.size() << "\n";
-#endif
-
     ast * r = m_ast_table.insert_if_not_there(n);
     SASSERT(r->m_hash == h);
     if (r != n) {
-#if 0
-        static unsigned reused = 0;
-        reused++;
-        if (reused % 100000 == 0)
-            verbose_stream() << "[ast-table] reused: " << reused << "\n";
-#endif
         SASSERT(contains);
         SASSERT(m_ast_table.contains(n));
         if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) {
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index 3bb963a7f..71a9079a0 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -687,7 +687,7 @@ br_status poly_rewriter<Config>::mk_sub(unsigned num_args, expr * const * args,
     }
     set_curr_sort(m().get_sort(args[0]));
     expr_ref minus_one(mk_numeral(numeral(-1)), m());
-    ptr_buffer<expr> new_args;
+    expr_ref_buffer new_args(m());
     new_args.push_back(args[0]);
     for (unsigned i = 1; i < num_args; i++) {
         if (is_zero(args[i])) continue;
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index f0439a55c..fad424b90 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -277,16 +277,21 @@ namespace datalog {
         return get_max_var(has_var);
     }
 
-    void del_rule(horn_subsume_model_converter* mc, rule& r) {
+    void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable) {
         if (mc) {
             ast_manager& m = mc->get_manager();
             expr_ref_vector body(m);
-            for (unsigned i = 0; i < r.get_tail_size(); ++i) {
-                if (r.is_neg_tail(i)) {
-                    body.push_back(m.mk_not(r.get_tail(i)));
-                }
-                else {
-                    body.push_back(r.get_tail(i));
+            if (unreachable) {
+                body.push_back(m.mk_false());
+            }
+            else {
+                for (unsigned i = 0; i < r.get_tail_size(); ++i) {
+                    if (r.is_neg_tail(i)) {
+                        body.push_back(m.mk_not(r.get_tail(i)));
+                    }
+                    else {
+                        body.push_back(r.get_tail(i));
+                    }
                 }
             }
             TRACE("dl_dr", 
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index c560ee28e..6b689fd17 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -354,7 +354,7 @@ namespace datalog {
         unsigned get_max_rule_var(const rule& r);
     };
 
-    void del_rule(horn_subsume_model_converter* mc, rule& r);
+    void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable);
 
     void resolve_rule(rule_manager& rm,
                       replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, 
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
index 7bd35b4ef..8421a99ba 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
@@ -607,6 +607,9 @@ namespace datalog {
         rule_set * res = alloc(rule_set, m_context);
         if (transform_rules(source, *res)) {
             res->inherit_predicates(source);
+            TRACE("dl", 
+                  source.display(tout); 
+                  res->display(tout););
         } else {
             dealloc(res);
             res = 0;
diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index 30ff330ab..f1a4eb32b 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -426,7 +426,7 @@ namespace datalog {
 
         for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) {
             rule* r = m_inlined_rules.get_rule(i);
-            datalog::del_rule(m_mc, *r);
+            datalog::del_rule(m_mc, *r, true);
         }
     }
 
@@ -465,7 +465,7 @@ namespace datalog {
             }
         }
         if (modified) {
-            datalog::del_rule(m_mc, *r0);
+            datalog::del_rule(m_mc, *r0, true);
         }
 
         return modified;
@@ -488,9 +488,9 @@ namespace datalog {
         }
 
         if (something_done && m_mc) {
-            for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
-                if (inlining_allowed(orig, (*rit)->get_decl())) {
-                    datalog::del_rule(m_mc, **rit);
+            for (rule* r : orig) {
+                if (inlining_allowed(orig, r->get_decl())) {
+                    datalog::del_rule(m_mc, *r, true);
                 }
             }
         }
@@ -580,7 +580,7 @@ namespace datalog {
                 // nothing unifies with the tail atom, therefore the rule is unsatisfiable
                 // (we can say this because relation pred doesn't have any ground facts either)
                 res = 0;
-                datalog::del_rule(m_mc, *r);
+                datalog::del_rule(m_mc, *r, false);
                 return true;
             }
             if (!is_oriented_rewriter(inlining_candidate, strat)) {
@@ -590,7 +590,7 @@ namespace datalog {
                 goto process_next_tail;
             }
             if (!try_to_inline_rule(*r, *inlining_candidate, ti, res)) {
-                datalog::del_rule(m_mc, *r);
+                datalog::del_rule(m_mc, *r, false);
                 res = 0;
             }
             return true;
@@ -823,7 +823,7 @@ namespace datalog {
                 if (num_tail_unifiers == 1) {
                     TRACE("dl", tout << "setting invalid: " << j << "\n";);
                     valid.set(j, false);
-                    datalog::del_rule(m_mc, *r2);
+                    datalog::del_rule(m_mc, *r2, true);
                     del_rule(r2, j);
                 }
 
diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp
index c094e5520..dc11935e3 100644
--- a/src/muz/transforms/dl_mk_slice.cpp
+++ b/src/muz/transforms/dl_mk_slice.cpp
@@ -426,8 +426,8 @@ namespace datalog {
         bool change = true;
         while (change) {
             change = false;
-            for (unsigned i = 0; i < src.get_num_rules(); ++i) {
-                change = prune_rule(*src.get_rule(i)) || change;
+            for (rule* r : src) {
+                change = prune_rule(*r) || change;
             }
         }
     }
@@ -457,18 +457,19 @@ namespace datalog {
 
     void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) {
         expr_ref_vector conjs = get_tail_conjs(r);
-        for (unsigned j = 0; j < conjs.size(); ++j) {
-            expr* e = conjs[j].get();
+        for (expr * e : conjs) {
             expr_ref r(m);
             unsigned v;
             if (is_eq(e, v, r) && is_output(v) && m_var_is_sliceable[v]) {
                 TRACE("dl", tout << "is_eq: " << mk_pp(e, m) << " " << (m_solved_vars[v].get()?"solved":"new") << "\n";);
                 add_var(v);
                 if (!m_solved_vars[v].get()) { 
+                    TRACE("dl", tout << v << " is solved\n";);
                     add_free_vars(parameter_vars, r);
                     m_solved_vars[v] = r;
                 }
                 else {
+                    TRACE("dl", tout << v << " is used\n";);
                     // variables can only be solved once.
                     add_free_vars(used_vars, e);
                     add_free_vars(used_vars, m_solved_vars[v].get());
@@ -508,10 +509,9 @@ namespace datalog {
         // 
         uint_set used_vars, parameter_vars;
         solve_vars(r, used_vars, parameter_vars);
-        uint_set::iterator it = used_vars.begin(), end = used_vars.end();
-        for (; it != end; ++it) {     
-            if (*it < m_var_is_sliceable.size()) {
-                m_var_is_sliceable[*it] = false;
+        for (unsigned uv : used_vars) {
+            if (uv < m_var_is_sliceable.size()) {
+                m_var_is_sliceable[uv] = false;
             }
         }
         //
@@ -533,6 +533,9 @@ namespace datalog {
                 if (m_solved_vars[i].get()) {
                     m_var_is_sliceable[i] = false;
                 }
+                if (parameter_vars.contains(i)) {
+                    m_var_is_sliceable[i] = false;
+                }
             }
             else if (is_output) {
                 if (parameter_vars.contains(i)) {
@@ -687,11 +690,9 @@ namespace datalog {
     }
 
     void mk_slice::display(std::ostream& out) {
-        obj_map<func_decl, bit_vector>::iterator it  = m_sliceable.begin();
-        obj_map<func_decl, bit_vector>::iterator end = m_sliceable.end();
-        for (; it != end; ++it) {
-            out << it->m_key->get_name() << " ";
-            bit_vector const& bv = it->m_value;
+        for (auto const& kv : m_sliceable) {
+            out << kv.m_key->get_name() << " ";
+            bit_vector const& bv = kv.m_value;
             for (unsigned i = 0; i < bv.size(); ++i) {
                 out << (bv.get(i)?"1":"0");
             }
diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp
index e26f105c6..c6bb2864b 100644
--- a/src/muz/transforms/dl_mk_subsumption_checker.cpp
+++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp
@@ -24,8 +24,10 @@ Revision History:
 #include "ast/rewriter/rewriter.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "muz/transforms/dl_mk_subsumption_checker.h"
-
 #include "muz/base/fixedpoint_params.hpp"
+#include "tactic/extension_model_converter.h"
+
+
 namespace datalog {
 
 
@@ -37,26 +39,28 @@ namespace datalog {
 
 
     bool mk_subsumption_checker::is_total_rule(const rule * r) {
-        if(r->get_tail_size()!=0) { return false; }
+        if (r->get_tail_size() != 0) { 
+            return false; 
+        }
 
         unsigned pt_len = r->get_positive_tail_size();
-        if(pt_len!=r->get_uninterpreted_tail_size()) {
-            //we dont' expect rules with negative tails to be total
+        if(pt_len != r->get_uninterpreted_tail_size()) {
+            // we dont' expect rules with negative tails to be total
             return false;
         }
 
-        for(unsigned i=0; i<pt_len; i++) {
+        for (unsigned i = 0; i < pt_len; i++) {
             func_decl * tail_pred = r->get_tail(i)->get_decl();
-            if(!m_total_relations.contains(tail_pred)) {
-                //this rule has a non-total predicate in the tail
+            if (!m_total_relations.contains(tail_pred)) {
+                // this rule has a non-total predicate in the tail
                 return false;
             }
         }
 
         unsigned t_len = r->get_positive_tail_size();
-        for(unsigned i=pt_len; i<t_len; i++) {
+        for(unsigned i = pt_len; i < t_len; i++) {
             SASSERT(!r->is_neg_tail(i)); //we assume interpreted tail not to be negated
-            if(!m.is_true(r->get_tail(i))) {
+            if (!m.is_true(r->get_tail(i))) {
                 //this rule has an interpreted tail which is not constant true
                 return false;
             }
@@ -183,20 +187,15 @@ namespace datalog {
         rule_ref_vector orig_rules(m_context.get_rule_manager());
         orig_rules.append(orig.get_num_rules(), orig.begin());
 
-        rule * * rbegin = orig_rules.c_ptr();
-        rule * * rend = rbegin + orig_rules.size();
-
         //before traversing we sort rules so that the shortest are in the beginning.
         //this will help make subsumption checks more efficient
-        std::sort(rbegin, rend, rule_size_comparator);
+        std::sort(orig_rules.c_ptr(), orig_rules.c_ptr() + orig_rules.size(), rule_size_comparator);
 
-        for(rule_set::iterator rit = rbegin; rit!=rend; ++rit) {
-
-            rule * r = *rit;
+        for (rule * r : orig_rules) {
             func_decl * head_pred = r->get_decl();
 
-            if(m_total_relations.contains(head_pred)) {
-                if(!orig.is_output_predicate(head_pred) ||
+            if (m_total_relations.contains(head_pred)) {
+                if (!orig.is_output_predicate(head_pred) ||
                         total_relations_with_included_rules.contains(head_pred)) {
                     //We just skip definitions of total non-output relations as 
                     //we'll eliminate them from the problem.
@@ -205,8 +204,7 @@ namespace datalog {
                     modified = true;
                     continue;
                 }
-                rule * defining_rule;
-                VERIFY(m_total_relation_defining_rules.find(head_pred, defining_rule));
+                rule * defining_rule = m_total_relation_defining_rules.find(head_pred);
                 if (defining_rule) {
                     rule_ref totality_rule(m_context.get_rule_manager());
                     VERIFY(transform_rule(defining_rule, subs_index, totality_rule));
@@ -224,24 +222,31 @@ namespace datalog {
             }
 
             rule_ref new_rule(m_context.get_rule_manager());
-            if(!transform_rule(r, subs_index, new_rule)) {
+            if (!transform_rule(r, subs_index, new_rule)) {
                 modified = true;
                 continue;
             }
-            if(m_new_total_relation_discovery_during_transformation && is_total_rule(new_rule)) {
+            if (m_new_total_relation_discovery_during_transformation && is_total_rule(new_rule)) {
                 on_discovered_total_relation(head_pred, new_rule.get());
             }
-            if(subs_index.is_subsumed(new_rule)) {
+            if (subs_index.is_subsumed(new_rule)) {
                 modified = true;
                 continue;
             }
-            if(new_rule.get()!=r) {
+            if (new_rule.get()!=r) {
                 modified = true;
             }
             tgt.add_rule(new_rule);
             subs_index.add(new_rule);
         }
         tgt.inherit_predicates(orig);
+        if (!m_total_relations.empty() && m_context.get_model_converter()) {
+            extension_model_converter* mc0 = alloc(extension_model_converter, m);
+            for (func_decl* p : m_total_relations) {
+                mc0->insert(p, m.mk_true());
+            }
+            m_context.add_model_converter(mc0);
+        }
         TRACE("dl",
             tout << "original set size: "<<orig.get_num_rules()<<"\n"
                  << "reduced set size: "<<tgt.get_num_rules()<<"\n"; );
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 257331161..01806bc24 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -20,7 +20,6 @@ Revision History:
 #include "qe/qe_lite.h"
 #include "ast/expr_abstract.h"
 #include "ast/used_vars.h"
-#include "ast/occurs.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
@@ -39,6 +38,30 @@ Revision History:
 #include "qe/qe_vartest.h"
 
 namespace eq {
+
+    bool occurs_var(unsigned idx, expr* e) {
+        ptr_buffer<expr> todo;
+        todo.push_back(e);        
+        ast_mark mark;
+        while (!todo.empty()) {
+            expr* e = todo.back();
+            todo.pop_back();
+            if (mark.is_marked(e)) continue;
+            mark.mark(e, true);
+            if (is_var(e)) {
+                if (to_var(e)->get_idx() == idx) return true;
+            }
+            else if (is_app(e)) {
+                todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+            }
+            else if (is_quantifier(e)) {
+                quantifier* q = to_quantifier(e);
+                if (occurs_var(idx + q->get_num_decls(), q->get_expr())) return true;
+            }
+        }
+        return false;
+    }
+
     class der {
         ast_manager &   m;
         arith_util      a;
@@ -65,7 +88,7 @@ namespace eq {
             for (unsigned i = 0; i < definitions.size(); i++) {
                 var * v  = vars[i];
                 expr * t = definitions[i];
-                if (t == 0 || has_quantifiers(t) || occurs(v, t))
+                if (t == 0 || has_quantifiers(t) || occurs_var(v->get_idx(), t))
                     definitions[i] = 0;
                 else
                     found = true; // found at least one candidate
@@ -679,9 +702,9 @@ namespace eq {
         }
 
         bool is_unconstrained(var* x, expr* t, unsigned i, expr_ref_vector const& conjs) {
-            bool occ = occurs(x, t);
+            bool occ = occurs_var(x->get_idx(), t);
             for (unsigned j = 0; !occ && j < conjs.size(); ++j) {
-                occ = (i != j) && occurs(x, conjs[j]);
+                occ = (i != j) && occurs_var(x->get_idx(), conjs[j]);
             }
             return !occ;
         }
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 7b508c7d8..2e65fddc9 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4373,7 +4373,7 @@ namespace smt {
     void context::add_rec_funs_to_model() {
         ast_manager& m = m_manager;
         SASSERT(m_model);
-        for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) {
+        for (unsigned i = 0; !get_cancel_flag() && i < m_asserted_formulas.get_num_formulas(); ++i) {
             expr* e = m_asserted_formulas.get_formula(i);
             if (is_quantifier(e)) {
                 TRACE("context", tout << mk_pp(e, m) << "\n";);
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 3cc577b29..c6cca2c43 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -209,7 +209,12 @@ namespace smt {
             ~scoped_mk_model() {
                 if (m_ctx.m_proto_model.get() != 0) {
                     m_ctx.m_model = m_ctx.m_proto_model->mk_model();
-                    m_ctx.add_rec_funs_to_model();
+                    try {
+                        m_ctx.add_rec_funs_to_model();
+                    }
+                    catch (...) {
+                        // no op
+                    }
                     m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
                 }
             }
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index a1f0f9777..ed926a50d 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -47,6 +47,8 @@ namespace smt {
         sLevel(0),
         finalCheckProgressIndicator(false),
         m_trail(m),
+        m_factory(nullptr),
+        m_unused_id(0),
         m_delayed_axiom_setup_terms(m),
         tmpStringVarCount(0),
         tmpXorVarCount(0),
@@ -61,8 +63,8 @@ namespace smt {
         cacheHitCount(0),
         cacheMissCount(0),
         m_fresh_id(0),
-        m_find(*this),
-        m_trail_stack(*this)
+        m_trail_stack(*this),
+        m_find(*this)
     {
         initialize_charset();
     }
@@ -279,7 +281,7 @@ namespace smt {
         } else {
             theory_var v = theory::mk_var(n);
             m_find.mk_var();
-            TRACE("str", tout << "new theory var v#" << v << std::endl;);
+            TRACE("str", tout << "new theory var v#" << v << " find " << m_find.find(v) << std::endl;);
             get_context().attach_th_var(n, this, v);
             get_context().mark_as_relevant(n);
             return v;
@@ -1903,8 +1905,8 @@ namespace smt {
 
     // support for user_smt_theory-style EQC handling
 
-    app * theory_str::get_ast(theory_var i) {
-        return get_enode(i)->get_owner();
+    app * theory_str::get_ast(theory_var v) {
+        return get_enode(v)->get_owner();
     }
 
     theory_var theory_str::get_var(expr * n) const {
@@ -4648,14 +4650,20 @@ namespace smt {
     // We only check m_find for a string constant.
 
     expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) {
-        expr * curr = n;
-        do {
-            if (u.str.is_string(curr)) {
-                hasEqcValue = true;
-                return curr;
-            }
-            curr = get_eqc_next(curr);
-        } while (curr != n);
+        theory_var curr = get_var(n);
+        if (curr != null_theory_var) {
+            curr = m_find.find(curr);
+            theory_var first = curr;
+            do {
+                expr* a = get_ast(curr);
+                if (u.str.is_string(a)) {
+                    hasEqcValue = true;
+                    return a;
+                }
+                curr = m_find.next(curr);
+            } 
+            while (curr != first && curr != null_theory_var);
+        }
         hasEqcValue = false;
         return n;
     }
@@ -10584,7 +10592,9 @@ namespace smt {
             return alloc(expr_wrapper_proc, val);
         } else {
             TRACE("str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;);
-            return alloc(expr_wrapper_proc, to_app(mk_string("**UNUSED**")));
+            std::ostringstream unused;
+            unused << "**UNUSED**" << (m_unused_id++);
+            return alloc(expr_wrapper_proc, to_app(mk_string(unused.str().c_str())));
         }
     }
 
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index acac8cad1..03fd31162 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -267,6 +267,10 @@ protected:
 
     str_value_factory * m_factory;
 
+    // Unique identifier appended to unused variables to ensure that model construction
+    // does not introduce equalities when they weren't enforced.
+    unsigned m_unused_id;
+
     // terms we couldn't go through set_up_axioms() with because they weren't internalized
     expr_ref_vector m_delayed_axiom_setup_terms;
 
@@ -358,8 +362,8 @@ protected:
     // cache mapping each string S to Length(S)
     obj_map<expr, app*> length_ast_map;
 
-    th_union_find m_find;
     th_trail_stack m_trail_stack;
+    th_union_find m_find;
     theory_var get_var(expr * n) const;
     expr * get_eqc_next(expr * n);
     app * get_ast(theory_var i);
diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp
index 651000297..c66483750 100644
--- a/src/tactic/arith/diff_neq_tactic.cpp
+++ b/src/tactic/arith/diff_neq_tactic.cpp
@@ -95,13 +95,13 @@ class diff_neq_tactic : public tactic {
             if (is_uninterp_const(lhs) && u.is_numeral(rhs, k) && m_max_neg_k <= k && k <= m_max_k) {
                 var x  = mk_var(lhs);
                 int _k = static_cast<int>(k.get_int64());
-                m_upper[x] = _k;
+                m_upper[x] = std::min(m_upper[x], _k);
                 
             }
             else if (is_uninterp_const(rhs) && u.is_numeral(lhs, k) && m_max_neg_k <= k && k <= m_max_k) {
                 var x  = mk_var(rhs);
                 int _k = static_cast<int>(k.get_int64()); 
-                m_lower[x] = _k;
+                m_lower[x] = std::max(m_lower[x], _k);
             }
             else {
                 throw_not_supported();
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 6d2cbea7d..1f1054bb6 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -1157,7 +1157,7 @@ public:
 
     bool explanation_is_correct(const vector<std::pair<mpq, unsigned>>& explanation) const {
 #ifdef Z3DEBUG
-        lconstraint_kind kind;
+        lconstraint_kind kind = EQ; // initialize it just to avoid a warning
         SASSERT(the_relations_are_of_same_type(explanation, kind));
         SASSERT(the_left_sides_sum_to_zero(explanation));
         mpq rs = sum_of_right_sides_of_explanation(explanation);
diff --git a/src/util/union_find.h b/src/util/union_find.h
index 7a99b149e..416b653af 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -102,6 +102,7 @@ public:
 
     unsigned find(unsigned v) const {
         while (true) {
+            SASSERT(v < m_find.size());
             unsigned new_v = m_find[v];
             if (new_v == v)
                 return v;