diff --git a/CMakeLists.txt b/CMakeLists.txt
index 188d8dfde..e5619ddc5 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -189,7 +189,6 @@ endif()
 # Note for some reason we have to leave off ``-D`` here otherwise
 # we get ``-D-DZ3DEBUG`` passed to the compiler
 list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:Z3DEBUG>)
-list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:LEAN_DEBUG>)
 list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Release>:_EXTERNAL_RELEASE>)
 list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEASE>)
 
@@ -272,45 +271,6 @@ list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS
   "${CMAKE_SOURCE_DIR}/src"
 )
 
-################################################################################
-# Linux specific configuration
-################################################################################
-if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux")
-  # Try to detect if it is necessary to link against librt.
-  # Note that glibc < 2.17 required librt to be linked to use clock_gettime()
-  # and friends.
-  set(CLOCK_GETTIME_REQUIRES_LIBRT_TEST_CODE
-    "
-    #include <time.h>
-    int main() {
-      timespec res;
-      int result = clock_gettime(CLOCK_REALTIME, &res);
-      return result == 0;
-    }
-    "
-  )
-  check_cxx_source_compiles(
-    "${CLOCK_GETTIME_REQUIRES_LIBRT_TEST_CODE}"
-    CLOCK_GETTIME_NO_REQUIRE_LIBRT
-  )
-  if (NOT CLOCK_GETTIME_NO_REQUIRE_LIBRT)
-    # Try again with librt
-    message(STATUS "Failed to link against clock_gettime(), trying with librt")
-    set(CMAKE_REQUIRED_LIBRARIES_OLD "${CMAKE_REQUIRED_LIBRARIES}")
-    set(CMAKE_REQUIRED_LIBRARIES "${CMAKE_REQUIRED_LIBRARIES} rt")
-    check_cxx_source_compiles(
-      "${CLOCK_GETTIME_REQUIRES_LIBRT_TEST_CODE}"
-      CLOCK_GETTIME_REQUIRES_LIBRT
-    )
-    set(CMAKE_REQUIRED_LIBRARIES "${CMAKE_REQUIRED_LIBRARIES_OLD}")
-    if (CLOCK_GETTIME_REQUIRES_LIBRT)
-      list(APPEND Z3_DEPENDENT_LIBS "rt")
-    else()
-      message(FATAL_ERROR "Failed to link against clock_gettime()")
-    endif()
-  endif()
-endif()
-
 ################################################################################
 # GNU multiple precision library support
 ################################################################################
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 2e827a7f3..ffbf13010 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2832,24 +2832,18 @@ def mk_config():
             CXXFLAGS       = '%s -D_LINUX_' % CXXFLAGS
             OS_DEFINES     = '-D_LINUX_'
             SO_EXT         = '.so'
-            LDFLAGS        = '%s -lrt' % LDFLAGS
             SLIBFLAGS      = '-shared'
-            SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
             SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
         elif sysname == 'FreeBSD':
             CXXFLAGS       = '%s -D_FREEBSD_' % CXXFLAGS
             OS_DEFINES     = '-D_FREEBSD_'
             SO_EXT         = '.so'
-            LDFLAGS        = '%s -lrt' % LDFLAGS
             SLIBFLAGS      = '-shared'
-            SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
         elif sysname == 'NetBSD':
             CXXFLAGS       = '%s -D_NETBSD_' % CXXFLAGS
             OS_DEFINES     = '-D_NETBSD_'
             SO_EXT         = '.so'
-            LDFLAGS        = '%s -lrt' % LDFLAGS
             SLIBFLAGS      = '-shared'
-            SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
         elif sysname == 'OpenBSD':
             CXXFLAGS       = '%s -D_OPENBSD_' % CXXFLAGS
             OS_DEFINES     = '-D_OPENBSD_'
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 0937e668e..8fba5e9f6 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -15,7 +15,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index 7c0143201..491fb8354 100644
--- a/src/api/api_tactic.cpp
+++ b/src/api/api_tactic.cpp
@@ -52,7 +52,9 @@ extern "C" {
         RESET_ERROR_CODE();
         tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name));
         if (t == nullptr) {
-            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+            std::stringstream err;
+            err << "unknown tactic " << name;
+            SET_ERROR_CODE(Z3_INVALID_ARG, err.str().c_str());
             RETURN_Z3(nullptr);
         }
         tactic * new_t = t->mk(mk_c(c)->m());
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 6113fdbe9..fb0657aa2 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -996,6 +996,7 @@ namespace z3 {
         bool is_implies() const { return is_app() && Z3_OP_IMPLIES  == decl().decl_kind(); }
         bool is_eq() const { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
         bool is_ite() const { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
+        bool is_distinct() const { return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
 
         friend expr distinct(expr_vector const& args);
         friend expr concat(expr const& a, expr const& b);
@@ -2387,7 +2388,7 @@ namespace z3 {
             return *this;
         }
         void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
-        // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
+        void add(expr_vector const& v) { check_context(*this, v); for (unsigned i = 0; i < v.size(); ++i) add(v[i]); }
         unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
         expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
         Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
index 211c67953..d361815b2 100644
--- a/src/ast/array_decl_plugin.cpp
+++ b/src/ast/array_decl_plugin.cpp
@@ -299,7 +299,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
         sort* srt2 = domain[i+1];
         if (!m_manager->compatible_sorts(srt1, srt2)) {
             std::stringstream strm;
-            strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt2, *m_manager) << " do not match";
+            strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt1, *m_manager) << " do not match";
             m_manager->raise_exception(strm.str());
             UNREACHABLE();
             return nullptr;
@@ -576,6 +576,27 @@ func_decl * array_recognizers::get_as_array_func_decl(func_decl * f) const {
     return to_func_decl(f->get_parameter(0).get_ast()); 
 }
 
+bool array_recognizers::is_const(expr* e, expr*& v) const {
+    return is_const(e) && (v = to_app(e)->get_arg(0), true);
+}
+
+bool array_recognizers::is_store_ext(expr* _e, expr_ref& a, expr_ref_vector& args, expr_ref& value) {
+    ast_manager& m = a.m();
+    if (is_store(_e)) {
+        app* e = to_app(_e);
+        a = e->get_arg(0);
+        unsigned sz = e->get_num_args();
+        args.reset();
+        for (unsigned i = 1; i < sz-1; ++i) {
+            args.push_back(e->get_arg(i));
+        }
+        value = e->get_arg(sz-1);
+        return true;
+    }
+    return false;
+}
+
+
 array_util::array_util(ast_manager& m): 
     array_recognizers(m.mk_family_id("array")),
     m_manager(m) {
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index c735fb811..5b44d31c9 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -152,6 +152,10 @@ public:
     bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
     func_decl * get_as_array_func_decl(expr * n) const;
     func_decl * get_as_array_func_decl(func_decl* f) const;
+
+    bool is_const(expr* e, expr*& v) const;
+
+    bool is_store_ext(expr* e, expr_ref& a, expr_ref_vector& args, expr_ref& value);
 };
 
 class array_util : public array_recognizers {
diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp
index e8d75f461..61bd9370c 100644
--- a/src/ast/expr_substitution.cpp
+++ b/src/ast/expr_substitution.cpp
@@ -65,8 +65,8 @@ std::ostream& expr_substitution::display(std::ostream& out) {
 }
 
 void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) {
-    obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, 0); 
-    if (entry->get_data().m_value == 0) {
+    obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, nullptr); 
+    if (entry->get_data().m_value == nullptr) {
         // new entry
         m_manager.inc_ref(c);
         m_manager.inc_ref(def);
@@ -89,14 +89,14 @@ void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_depend
         entry->get_data().m_value = def;
         if (proofs_enabled()) {
             obj_map<expr, proof*>::obj_map_entry * entry_pr = m_subst_pr->find_core(c);
-            SASSERT(entry_pr != 0);
+            SASSERT(entry_pr != nullptr);
             m_manager.inc_ref(def_pr);
             m_manager.dec_ref(entry_pr->get_data().m_value);
             entry_pr->get_data().m_value = def_pr;
         }
         if (unsat_core_enabled()) {
             obj_map<expr, expr_dependency*>::obj_map_entry * entry_dep = m_subst_dep->find_core(c);
-            SASSERT(entry_dep != 0);
+            SASSERT(entry_dep != nullptr);
             m_manager.inc_ref(def_dep);
             m_manager.dec_ref(entry_dep->get_data().m_value);
             entry_dep->get_data().m_value = def_dep;
diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index 56e094dab..6ad9c3654 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -230,105 +230,98 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
 }
 
 br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
-    SASSERT(num_args >= 0);
-    bool is_store0 = m_util.is_store(args[0]);
-    bool is_const0 = m_util.is_const(args[0]);
-    if (num_args == 1) {
-        //
-        // map_f (store a j v) = (store (map_f a) j (f v)) 
-        //
-        if (is_store0) {
-            app * store_expr = to_app(args[0]);
-            unsigned num_args = store_expr->get_num_args();
-            SASSERT(num_args >= 3);
-            expr * a = store_expr->get_arg(0);
-            expr * v = store_expr->get_arg(num_args-1);
-            
-            ptr_buffer<expr> new_args;
-            
-            new_args.push_back(m_util.mk_map(f, 1, &a)); // (map_f a)
-            new_args.append(num_args - 2, store_expr->get_args() + 1); // j
-            new_args.push_back(m().mk_app(f, v));   // (f v)
-            
-            result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr());
-            return BR_REWRITE2;
-        }
-        
-        //
-        // map_f (const v) = (const (f v))
-        //
-        if (is_const0) {
-            expr * fv = m().mk_app(f, to_app(args[0])->get_arg(0));
-            result = m_util.mk_const_array(m().get_sort(args[0]), fv);
-            return BR_REWRITE2;
-        }
-        return BR_FAILED;
-    }
 
-    SASSERT(num_args > 1);
-    
-    if (is_store0) {
-        unsigned num_indices = to_app(args[0])->get_num_args() - 2;
-        unsigned i;
-        for (i = 1; i < num_args; i++) {
-            if (!m_util.is_store(args[i]))
-                break;
-            unsigned j;
-            for (j = 1; j < num_indices+1; j++) {
-                if (to_app(args[0])->get_arg(j) != to_app(args[i])->get_arg(j))
-                    break;
-            }
-            if (j < num_indices+1)
-                break;
+    app* store_expr = nullptr;
+    unsigned num_indices = 0;
+    bool same_store = true;
+    for (unsigned i = 0; same_store && i < num_args; i++) {
+        expr* a = args[i];
+        if (m_util.is_const(a)) {
+            continue;
         }
-        //
-        // map_f (store a_1 j v_1) ... (store a_n j v_n) --> (store (map_f a_1 ... a_n) j (f v_1 ... v_n))
-        //
-        if (i == num_args) {
-            ptr_buffer<expr> arrays;
-            ptr_buffer<expr> values;
-            for (unsigned i = 0; i < num_args; i++) {
-                arrays.push_back(to_app(args[i])->get_arg(0));
-                values.push_back(to_app(args[i])->get_arg(num_indices+1));
+        else if (!m_util.is_store(a)) {
+            same_store = false;
+        }
+        else if (!store_expr) {
+            num_indices = to_app(a)->get_num_args() - 2;
+            store_expr = to_app(a);
+        }
+        else {
+            for (unsigned j = 1; same_store && j < num_indices + 1; j++) {
+                same_store = (store_expr->get_arg(j) == to_app(a)->get_arg(j));
             }
+        }
+    }
+    
+    //
+    // map_f (store a_1 j v_1) ... (store a_n j v_n) --> (store (map_f a_1 ... a_n) j (f v_1 ... v_n))
+    //
+    if (same_store) {
+        ptr_buffer<expr> arrays;
+        ptr_buffer<expr> values;
+        for (unsigned i = 0; i < num_args; i++) {
+            expr* a = args[i];
+            if (m_util.is_const(a)) {
+                arrays.push_back(a);
+                values.push_back(to_app(a)->get_arg(0));
+            }
+            else {
+                arrays.push_back(to_app(a)->get_arg(0));
+                values.push_back(to_app(a)->get_arg(num_indices+1));
+            }
+        }
+        if (store_expr) {
             ptr_buffer<expr> new_args;
             new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr()));
             new_args.append(num_indices, to_app(args[0])->get_args() + 1);
             new_args.push_back(m().mk_app(f, values.size(), values.c_ptr()));
             result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr());
-            return BR_REWRITE2;
         }
-        return BR_FAILED;
+        else {
+            expr_ref value(m().mk_app(f, values.size(), values.c_ptr()), m());
+            sort* s0 = m().get_sort(args[0]);
+            unsigned sz = get_array_arity(s0);
+            ptr_vector<sort> domain;
+            for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i));
+            sort_ref s(m_util.mk_array_sort(sz, domain.c_ptr(), m().get_sort(value)), m());
+            result = m_util.mk_const_array(s, value);
+        }
+        return BR_REWRITE2;
     }
 
-    if (is_const0) {
-        unsigned i;
-        for (i = 1; i < num_args; i++) {
-            if (!m_util.is_const(args[i]))
-                break;
+    //
+    // map_f (lambda x1 b1) ... (lambda x1 bn) -> lambda x1 (f b1 .. bn)
+    //
+    quantifier* lam = nullptr;
+    for (unsigned i = 0; i < num_args; ++i) {
+        if (is_lambda(args[i])) {
+            lam = to_quantifier(args[i]);
         }
-        if (i == num_args) {
-            //
-            // map_f (const v_1) ... (const v_n) = (const (f v_1 ... v_n))
-            //
-            ptr_buffer<expr> values;
-            for (unsigned i = 0; i < num_args; i++) {
-                values.push_back(to_app(args[i])->get_arg(0));
+    }
+    if (lam) {
+        expr_ref_vector args1(m());
+        for (unsigned i = 0; i < num_args; ++i) {
+            expr* a = args[i];
+            if (m_util.is_const(a)) {
+                args1.push_back(to_app(a)->get_arg(0));
+            }
+            else if (is_lambda(a)) {
+                lam = to_quantifier(a);
+                args1.push_back(lam->get_expr());
+            }
+            else {
+                expr_ref_vector sel(m());
+                sel.push_back(a);
+                unsigned n = lam->get_num_decls();
+                for (unsigned i = 0; i < n; ++i) {
+                    sel.push_back(m().mk_var(n - i - 1, lam->get_decl_sort(i)));
+                }
+                args1.push_back(m_util.mk_select(sel.size(), sel.c_ptr()));
             }
-            
-            expr * fv = m().mk_app(f, values.size(), values.c_ptr());
-            sort * in_s = get_sort(args[0]);
-            ptr_vector<sort> domain;
-            unsigned domain_sz = get_array_arity(in_s);
-            for (unsigned i = 0; i < domain_sz; i++) 
-                domain.push_back(get_array_domain(in_s, i));
-            sort_ref out_s(m());
-            out_s = m_util.mk_array_sort(domain_sz, domain.c_ptr(), f->get_range());
-            parameter p(out_s.get());
-            result = m().mk_app(get_fid(), OP_CONST_ARRAY, 1, &p, 1, &fv);
-            return BR_REWRITE2;
         }
-        return BR_FAILED;
+        result = m().mk_app(f, args1.size(), args1.c_ptr());
+        result = m().update_quantifier(lam, result);
+        return BR_REWRITE3;        
     }
 
     return BR_FAILED;
@@ -396,10 +389,96 @@ br_status array_rewriter::mk_set_subset(expr * arg1, expr * arg2, expr_ref & res
     return BR_REWRITE3;
 }
 
+void array_rewriter::mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls) {
+    expr_ref tmp1(m()), tmp2(m());
+    expr_ref a(m()), v(m());
+    expr_ref_vector args0(m()), args(m());
+    while (m_util.is_store_ext(e, a, args0, v)) {                                        
+        args.reset();
+        args.push_back(lhs);
+        args.append(args0);
+        mk_select(args.size(), args.c_ptr(), tmp1);                     
+        args[0] = rhs;                                                  
+        mk_select(args.size(), args.c_ptr(), tmp2);                     
+        fmls.push_back(m().mk_eq(tmp1, tmp2));    
+        e = a;
+    }                                                
+}
+
+bool array_rewriter::has_index_set(expr* e, expr_ref& e0, vector<expr_ref_vector>& indices) {
+    expr_ref_vector args(m());
+    expr_ref a(m()), v(m());
+    a = e;
+    while (m_util.is_store_ext(e, a, args, v)) {
+        indices.push_back(args);
+        e = a;
+    }
+    e0 = e;
+    if (is_lambda(e0)) {
+        quantifier* q = to_quantifier(e0);
+        e = q->get_expr();
+        unsigned num_idxs = q->get_num_decls();
+        expr* e1, *e2, *e3;
+        ptr_vector<expr> eqs;
+        while (!is_ground(e) && m().is_ite(e, e1, e2, e3) && is_ground(e2)) {
+            args.reset();
+            args.resize(num_idxs, nullptr);
+            eqs.reset();
+            eqs.push_back(e1);
+            for (unsigned i = 0; i < eqs.size(); ++i) {
+                expr* e = eqs[i];
+                if (m().is_and(e)) {
+                    eqs.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+                }
+                else if (m().is_eq(e, e1, e2)) {
+                    if (is_var(e2)) {
+                        std::swap(e1, e2);
+                    }
+                    if (is_var(e1) && is_ground(e2)) {
+                        unsigned idx = to_var(e1)->get_idx();
+                        args[num_idxs - idx - 1] = e2;
+                    }
+                    else {
+                        return false;
+                    }
+                }                
+            }
+            for (unsigned i = 0; i < num_idxs; ++i) {
+                if (!args.get(i)) return false;
+            }
+            indices.push_back(args);
+            e = e3;
+        }
+        e0 = e;
+        return is_ground(e);
+    }
+    return true;
+}
+
 br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
     if (!m_expand_store_eq) {
         return BR_FAILED;
     }
+    expr_ref_vector fmls(m());
+
+#if 0
+    // lambda friendly version of array equality rewriting.
+    vector<expr_ref_vector> indices;
+    expr_ref lhs0(m()), rhs0(m());
+    expr_ref tmp1(m()), tmp2(m());
+    if (has_index_set(lhs, lhs0, indices) && has_index_set(rhs, rhs0, indices) && lhs0 == rhs0) {
+        expr_ref_vector args(m());
+        for (auto const& idxs : indices) {
+            args.reset();
+            args.push_back(lhs);
+            args.append(idxs);
+            mk_select(args.size(), args.c_ptr(), tmp1);
+            args[0] = rhs;
+            mk_select(args.size(), args.c_ptr(), tmp2);
+            fmls.push_back(m().mk_eq(tmp1, tmp2));
+        }
+    }
+#endif
     expr* lhs1 = lhs;
     while (m_util.is_store(lhs1)) {
         lhs1 = to_app(lhs1)->get_arg(0);
@@ -411,25 +490,9 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
     if (lhs1 != rhs1) {
         return BR_FAILED;
     }
-    ptr_buffer<expr> fmls, args;
-    expr* e;
-    expr_ref tmp1(m()), tmp2(m());
-#define MK_EQ()                                                         \
-    while (m_util.is_store(e)) {                                        \
-        args.push_back(lhs);                                            \
-        args.append(to_app(e)->get_num_args()-2,to_app(e)->get_args()+1); \
-        mk_select(args.size(), args.c_ptr(), tmp1);                     \
-        args[0] = rhs;                                                  \
-        mk_select(args.size(), args.c_ptr(), tmp2);                     \
-        fmls.push_back(m().mk_eq(tmp1, tmp2));                          \
-        e = to_app(e)->get_arg(0);                                      \
-        args.reset();                                                   \
-    }                                                \
-    
-    e = lhs;
-    MK_EQ();
-    e = rhs;
-    MK_EQ();
+
+    mk_eq(lhs, lhs, rhs, fmls);
+    mk_eq(rhs, lhs, rhs, fmls);
     result = m().mk_and(fmls.size(), fmls.c_ptr());
     return BR_REWRITE_FULL;
 }
diff --git a/src/ast/rewriter/array_rewriter.h b/src/ast/rewriter/array_rewriter.h
index 90b3b6f34..a951db725 100644
--- a/src/ast/rewriter/array_rewriter.h
+++ b/src/ast/rewriter/array_rewriter.h
@@ -35,6 +35,8 @@ class array_rewriter {
     bool          m_expand_select_ite;
     template<bool CHECK_DISEQ>
     lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2);
+    bool has_index_set(expr* e, expr_ref& e0, vector<expr_ref_vector>& indices);
+    void mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls);
 public:    
     array_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         m_util(m) {
diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp
index a599cfa4a..8819eb584 100644
--- a/src/cmd_context/eval_cmd.cpp
+++ b/src/cmd_context/eval_cmd.cpp
@@ -71,6 +71,7 @@ public:
         expr_ref r(ctx.m());
         unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
         unsigned rlimit  = m_params.get_uint("rlimit", 0);
+        // md->compress();
         model_evaluator ev(*(md.get()), m_params);
         ev.set_solver(alloc(th_solver, ctx));
         cancel_eh<reslimit> eh(ctx.m().limit());
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index d2f14d9b4..b2b927faf 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -37,7 +37,7 @@ Revision History:
 #include "model/model_smt2_pp.h"
 #include "ast/rewriter/var_subst.h"
 
-
+namespace {
 struct evaluator_cfg : public default_rewriter_cfg {
     ast_manager &                   m;
     model_core &                    m_model;
@@ -54,7 +54,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
     unsigned long long              m_max_memory;
     unsigned                        m_max_steps;
     bool                            m_model_completion;
-    bool                            m_cache;
     bool                            m_array_equalities;
     bool                            m_array_as_stores;
     obj_map<func_decl, expr*>       m_def_cache;
@@ -92,7 +91,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
         model_evaluator_params p(_p);
         m_max_memory       = megabytes_to_bytes(p.max_memory());
         m_max_steps        = p.max_steps();
-        m_cache            = p.cache();
         m_model_completion = p.completion();
         m_array_equalities = p.array_equalities();
         m_array_as_stores  = p.array_as_stores();
@@ -340,8 +338,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return num_steps > m_max_steps;
     }
 
-    bool cache_results() const { return m_cache; }
-
     br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
         TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << "\n";);
         if (a == b) {
@@ -556,8 +552,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return true;
     }
 };
-
-template class rewriter_tpl<evaluator_cfg>;
+}
 
 struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
     evaluator_cfg m_cfg;
@@ -569,6 +564,11 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
         set_cancel_check(false);
     }
     void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);}
+    void reset() {
+        rewriter_tpl<evaluator_cfg>::reset();
+        m_cfg.reset();
+        m_cfg.m_def_cache.reset();
+    }
 };
 
 model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
@@ -592,7 +592,10 @@ void model_evaluator::get_param_descrs(param_descrs & r) {
 }
 
 void model_evaluator::set_model_completion(bool f) {
-    m_imp->cfg().m_model_completion = f;
+    if (m_imp->cfg().m_model_completion != f) {
+        reset();
+        m_imp->cfg().m_model_completion = f;
+    }
 }
 
 bool model_evaluator::get_model_completion() const {
@@ -609,8 +612,8 @@ unsigned model_evaluator::get_num_steps() const {
 
 void model_evaluator::cleanup(params_ref const & p) {
     model_core & md = m_imp->cfg().m_model;
-    dealloc(m_imp);
-    m_imp = alloc(imp, md, p);
+    m_imp->~imp();
+    new (m_imp) imp(md, p);
 }
 
 void model_evaluator::reset(params_ref const & p) {
@@ -619,8 +622,8 @@ void model_evaluator::reset(params_ref const & p) {
 }
 
 void model_evaluator::reset(model_core &model, params_ref const& p) {
-    dealloc(m_imp);
-    m_imp = alloc(imp, model, p);
+    m_imp->~imp();
+    new (m_imp) imp(model, p);
 }
 
 
diff --git a/src/model/model_evaluator_params.pyg b/src/model/model_evaluator_params.pyg
index 509b3e7c7..890e19cfe 100644
--- a/src/model/model_evaluator_params.pyg
+++ b/src/model/model_evaluator_params.pyg
@@ -3,7 +3,6 @@ def_module_params('model_evaluator',
                   params=(max_memory_param(),
                           max_steps_param(),
                           ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'),
-                          ('cache', BOOL, True, 'cache intermediate results in the model evaluator'),
                           ('array_equalities', BOOL, True, 'evaluate array equalities'),
                           ('array_as_stores', BOOL, True, 'return array as a set of stores'),
                           ))
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 76e7e24c6..04f5834aa 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2948,7 +2948,7 @@ proof_ref context::get_ground_refutation() {
     ground_sat_answer_op op(*this);
     return op(*m_query);
 }
-expr_ref context::get_ground_sat_answer() const {
+expr_ref context::get_ground_sat_answer()  {
     if (m_last_result != l_true) {
         IF_VERBOSE(0, verbose_stream()
                    << "Sat answer unavailable when result is false\n";);
@@ -2994,6 +2994,7 @@ expr_ref context::get_ground_sat_answer() const {
     ref<solver> cex_ctx =
         mk_smt_solver(m, params_ref::get_empty(), symbol::null);
 
+    bool first = true;
     // preorder traversal of the query derivation tree
     for (unsigned curr = 0; curr < pts.size (); curr++) {
         // pick next pt, fact, and cex_fact
@@ -3032,6 +3033,7 @@ expr_ref context::get_ground_sat_answer() const {
         }
         cex_ctx->assert_expr(pt->transition());
         cex_ctx->assert_expr(pt->rule2tag(r));
+        TRACE("cex", cex_ctx->display(tout););
         lbool res = cex_ctx->check_sat(0, nullptr);
         CTRACE("cex", res == l_false,
                tout << "Cex fact: " << mk_pp(cex_fact, m) << "\n";
@@ -3046,6 +3048,19 @@ expr_ref context::get_ground_sat_answer() const {
         cex_ctx->get_model (local_mdl);
         cex_ctx->pop (1);
         local_mdl->set_model_completion(true);
+        if (first) {
+            unsigned sig_size = pt->sig_size();
+            expr_ref_vector ground_fact_conjs(m);
+            expr_ref_vector ground_arg_vals(m);
+            for (unsigned j = 0; j < sig_size; j++) {
+                expr_ref sig_arg(m), sig_val(m);
+                sig_arg = m.mk_const (m_pm.o2n(pt->sig(j), 0));
+                sig_val = (*local_mdl)(sig_arg);
+                ground_arg_vals.push_back(sig_val);
+            }
+            cex.push_back(m.mk_app(pt->head(), sig_size, ground_arg_vals.c_ptr()));            
+            first = false;
+        }
         for (unsigned i = 0; i < child_pts.size(); i++) {
             pred_transformer& ch_pt = *(child_pts.get(i));
             unsigned sig_size = ch_pt.sig_size();
@@ -3073,10 +3088,10 @@ expr_ref context::get_ground_sat_answer() const {
 
     TRACE ("spacer", tout << "ground cex\n" << cex << "\n";);
 
-    return expr_ref(m.mk_and(cex.size(), cex.c_ptr()), m);
+    return mk_and(cex);
 }
 
-void context::display_certificate(std::ostream &out) const {
+void context::display_certificate(std::ostream &out)  {
     switch(m_last_result) {
     case l_false:
         out << mk_pp(mk_unsat_answer(), m);
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 494de1c23..54eb1befa 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -1010,7 +1010,7 @@ class context {
     /**
        \brief Retrieve satisfying assignment with explanation.
     */
-    expr_ref mk_sat_answer() const {return get_ground_sat_answer();}
+    expr_ref mk_sat_answer() {return get_ground_sat_answer();}
     expr_ref mk_unsat_answer() const;
     unsigned get_cex_depth ();
 
@@ -1086,7 +1086,7 @@ public:
      * get bottom-up (from query) sequence of ground predicate instances
      * (for e.g. P(0,1,0,0,3)) that together form a ground derivation to query
      */
-    expr_ref get_ground_sat_answer () const;
+    expr_ref get_ground_sat_answer ();
     proof_ref get_ground_refutation();
     void get_rules_along_trace (datalog::rule_ref_vector& rules);
 
@@ -1095,7 +1095,7 @@ public:
     void reset();
 
     std::ostream& display(std::ostream& out) const;
-    void display_certificate(std::ostream& out) const;
+    void display_certificate(std::ostream& out);
 
     pob& get_root() const {return m_pob_queue.get_root();}
     void set_query(func_decl* q) {m_query_pred = q;}
diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp
index f28864e27..114bc69b9 100644
--- a/src/muz/spacer/spacer_iuc_solver.cpp
+++ b/src/muz/spacer/spacer_iuc_solver.cpp
@@ -342,7 +342,7 @@ namespace spacer {
                     
                     proof_ref pr2(m);
                     {
-                        scoped_watch _t_ (m_hyp_reduce2_sw);
+                        // scoped_watch _t_ (m_hyp_reduce2_sw);
                         hypothesis_reducer hyp_reducer(m);
                         pr2 = hyp_reducer.reduce(pr1);
                     }
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 80a81ba3a..eb766a1ba 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -233,7 +233,8 @@ namespace opt {
         get_model(m_model);
         inf_eps val2;
         m_valid_objectives[i] = true;
-        TRACE("opt", tout << (has_shared?"has shared":"non-shared") << " " << val << "\n";);
+        has_shared = true;
+        TRACE("opt", tout << (has_shared?"has shared":"non-shared") << " " << val << " " << blocker << "\n";);
         if (!m_models[i]) {
             set_model(i);
         }
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 4a35acd02..462c9855a 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -215,7 +215,7 @@ namespace opt {
                     ++num_scopes;
                     bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));
                 }
-                TRACE("opt", tout << delta_per_step << " " << bound << "\n";);
+                TRACE("opt", tout << "delta: " << delta_per_step << " " << bound << "\n";);
                 m_s->assert_expr(bound);
             }
             else if (is_sat == l_false && delta_per_step > rational::one()) {
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index c103b0276..e09ea0f3c 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -2677,6 +2677,7 @@ namespace smt2 {
             m_ctx.regular_stream() << "(";
             expr ** expr_it  = expr_stack().c_ptr() + spos;
             expr ** expr_end = expr_it + m_cached_strings.size();
+            // md->compress();
             for (unsigned i = 0; expr_it < expr_end; expr_it++, i++) {
                 model::scoped_model_completion _scm(md, true);
                 expr_ref v = (*md)(*expr_it);
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 1f8f78aaa..4e2d8413a 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -2430,7 +2430,6 @@ class qe_lite_tactic : public tactic {
             tactic_report report("qe-lite", *g);
             proof_ref new_pr(m);
             expr_ref new_f(m);
-            bool produce_proofs = g->proofs_enabled();
 
             unsigned sz = g->size();
             for (unsigned i = 0; i < sz; i++) {
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index c6b04cfd8..427077804 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -42,8 +42,8 @@ namespace sat {
         m_checkpoint_enabled(true),
         m_config(p),
         m_par(nullptr),
-        m_cls_allocator_idx(false),
         m_drat(*this),
+        m_cls_allocator_idx(false),
         m_cleaner(*this),
         m_simplifier(*this, p),
         m_scc(*this, p),
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 45ade8b46..ceeb1617f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1101,24 +1101,6 @@ public:
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
 
-    // create axiom for 
-    //    u = v + r*w,
-    ///   abs(r) > r >= 0
-    void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r) {
-        app_ref term(m);
-        term = a.mk_sub(get_enode(u)->get_owner(), 
-                        a.mk_add(get_enode(v)->get_owner(),
-                                 a.mk_mul(a.mk_numeral(r, true), 
-                                          get_enode(w)->get_owner())));
-        theory_var z = internalize_def(term);
-        lp::var_index vi = get_var_index(z);
-        add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero()));
-        add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero()));
-        add_def_constraint(m_solver->add_var_bound(get_var_index(v), lp::GE, rational::zero()));
-        add_def_constraint(m_solver->add_var_bound(get_var_index(v), lp::LT, abs(r)));
-        TRACE("arith", m_solver->print_constraints(tout << term << "\n"););
-    }
-
     void mk_idiv_mod_axioms(expr * p, expr * q) {
         if (a.is_zero(q)) {
             return;
@@ -1679,12 +1661,31 @@ public:
      * 0 < q => (v(p)/v(q) <= p/q => v(p)/v(q) - 1 < n) 
      * 
      */
+
+    bool is_bounded(expr* n) {
+        expr* x = nullptr, *y = nullptr;
+        while (true) {
+            if (a.is_idiv(n, x, y) && a.is_numeral(y)) {
+                n = x;
+            }
+            else if (a.is_mod(n, x, y) && a.is_numeral(y)) {
+                return true;
+            }
+            else if (a.is_numeral(n)) {
+                return true;
+            }
+            else {
+                return false;
+            }
+        }
+    }
+
     bool check_idiv_bounds() {
         if (m_idiv_terms.empty()) {
             return true;
         }
-        bool all_divs_valid = true;        
         init_variable_values();
+        bool all_divs_valid = true;        
         for (expr* n : m_idiv_terms) {
             expr* p = nullptr, *q = nullptr;
             VERIFY(a.is_idiv(n, p, q));
@@ -1704,8 +1705,14 @@ public:
             }
 
             if (a.is_numeral(q, r2) && r2.is_pos()) {
-                if (get_value(v) == div(r1, r2)) continue;
+                rational val_v = get_value(v);
+                if (val_v == div(r1, r2)) continue;
+                if (!is_bounded(n)) {
+                    TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";);
+                    continue;
+                }
             
+                TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";);
                 rational div_r = div(r1, r2);
                 // p <= q * div(r1, q) + q - 1 => div(p, q) <= div(r1, r2)
                 // p >= q * div(r1, q) => div(r1, q) <= div(p, q)
@@ -1753,53 +1760,6 @@ public:
                       ctx().display_literals_verbose(tout, lits) << "\n";);                      
                 continue;
             }
-#if 0
-
-            // TBD similar for non-linear division.
-            // better to deal with in nla_solver:
-
-            all_divs_valid = false;
-
-        
-            //  
-            //    p/q <= r1/r2 => n <= div(r1, r2)
-            // <=>
-            //    p*r2 <= q*r1 => n <= div(r1, r2)
-            //
-            //    p/q >= r1/r2 => n >= div(r1, r2)
-            // <=>
-            //    p*r2 >= r1*q => n >= div(r1, r2)
-            // 
-            expr_ref zero(a.mk_int(0), m);
-            expr_ref divc(a.mk_numeral(div(r1, r2), true), m);
-            expr_ref pqr(a.mk_sub(a.mk_mul(a.mk_numeral(r2, true), p), a.mk_mul(a.mk_numeral(r1, true), q)), m);            
-            literal pq_lhs   = ~mk_literal(a.mk_le(pqr, zero));
-            literal pq_rhs   = ~mk_literal(a.mk_ge(pqr, zero));
-            literal n_le_div = mk_literal(a.mk_le(n, divc));
-            literal n_ge_div = mk_literal(a.mk_ge(n, divc)); 
-            if (m.has_trace_stream()) {
-                app_ref body(m);
-                body = m.mk_implies(ctx().bool_var2expr(pq_lhs.var()), ctx().bool_var2expr(n_le_div.var()));
-                th.log_axiom_instantiation(body);
-            }
-            mk_axiom(pq_lhs, n_le_div); 
-            if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) {
-                app_ref body(m);
-                body = m.mk_implies(ctx().bool_var2expr(pq_rhs.var()), ctx().bool_var2expr(n_ge_div.var()));
-                th.log_axiom_instantiation(body);
-            }
-            mk_axiom(pq_rhs, n_ge_div);
-            if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            TRACE("arith",
-                  literal_vector lits;
-                  lits.push_back(pq_lhs);
-                  lits.push_back(n_le_div);
-                  ctx().display_literals_verbose(tout, lits) << "\n";
-                  lits[0] = pq_rhs;
-                  lits[1] = n_ge_div;
-                  ctx().display_literals_verbose(tout, lits) << "\n";);
-#endif
         }
         
         return all_divs_valid;
@@ -1894,14 +1854,17 @@ public:
             TRACE("arith", tout << "canceled\n";);
             return l_undef;
         }
+
+        lbool lia_check = l_undef;
         if (!check_idiv_bounds()) {
-            TRACE("arith", tout << "idiv bounds check\n";);
             return l_false;
         }
         m_explanation.reset();
         switch (m_lia->check()) {
         case lp::lia_move::sat:
-            return l_true;
+            lia_check = l_true;
+            break;
+
         case lp::lia_move::branch: {
             TRACE("arith", tout << "branch\n";);
             app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
@@ -1917,7 +1880,8 @@ public:
             // TBD: ctx().force_phase(ctx().get_literal(b));
             // at this point we have a new unassigned atom that the 
             // SAT core assigns a value to
-            return l_false;
+            lia_check = l_false;
+            break;
         }
         case lp::lia_move::cut: {
             TRACE("arith", tout << "cut\n";);
@@ -1943,24 +1907,27 @@ public:
                   ctx().display_lemma_as_smt_problem(tout << "new cut:\n", m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
                   display(tout););
             assign(lit);
-            return l_false;
+            lia_check = l_false;
+            break;
         }
         case lp::lia_move::conflict:
             TRACE("arith", tout << "conflict\n";);
             // ex contains unsat core
             m_explanation = m_lia->get_explanation().m_explanation;
             set_conflict1();
-            return l_false;
+            lia_check = l_false;
+            break;
         case lp::lia_move::undef:
             TRACE("arith", tout << "lia undef\n";);
-            return l_undef;
+            lia_check = l_undef;
+            break;
         case lp::lia_move::continue_with_check:
-            return l_undef;
+            lia_check = l_undef;
+            break;
         default:
             UNREACHABLE();
         }
-        UNREACHABLE();
-        return l_undef;
+        return lia_check;
     }
 
     lbool check_nra() {
@@ -3332,10 +3299,10 @@ public:
             vi = m_theory_var2var_index[v];
             st = m_solver->maximize_term(vi, term_max);
         }
-        TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << " " << term_max << "\n"););
         switch (st) {
         case lp::lp_status::OPTIMAL: {
             init_variable_values();
+            TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
             inf_rational val = get_value(v);
             // inf_rational val(term_max.x, term_max.y);
             blocker = mk_gt(v);
@@ -3343,11 +3310,13 @@ public:
         }
         case lp::lp_status::FEASIBLE: {
             inf_rational val = get_value(v);
+            TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
             blocker = mk_gt(v);
             return inf_eps(rational::zero(), val);
         }
         default:
             SASSERT(st == lp::lp_status::UNBOUNDED);
+            TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
             has_shared = false;
             blocker = m.mk_false();
             return inf_eps(rational::one(), inf_rational());
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 50e666c70..37c5b6237 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1427,7 +1427,7 @@ namespace smt {
         // 0 < i < len(H) -->
         //     H = hd ++ tl
         //     len(hd) = i
-        //     str.indexof(tl, N, 0)
+        //     i + str.indexof(tl, N, 0)
 
         expr * H = nullptr; // "haystack"
         expr * N = nullptr; // "needle"
@@ -1463,12 +1463,19 @@ namespace smt {
             expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
             assert_implication(premise, conclusion);
         }
-        // case 4: 0 < i < len(H)
+        // case 3.5: H doesn't contain N
+        {
+            expr_ref premise(m.mk_not(u.str.mk_contains(H, N)), m);
+            expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
+            assert_implication(premise, conclusion);
+        }
+        // case 4: 0 < i < len(H) and H contains N
         {
             expr_ref premise1(m_autil.mk_gt(i, zero), m);
             //expr_ref premise2(m_autil.mk_lt(i, mk_strlen(H)), m);
             expr_ref premise2(m.mk_not(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero)), m);
-            expr_ref _premise(m.mk_and(premise1, premise2), m);
+            expr_ref premise3(u.str.mk_contains(H, N), m);
+            expr_ref _premise(m.mk_and(premise1, premise2, premise3), m);
             expr_ref premise(_premise);
             th_rewriter rw(m);
             rw(premise);
@@ -1479,7 +1486,8 @@ namespace smt {
             expr_ref_vector conclusion_terms(m);
             conclusion_terms.push_back(ctx.mk_eq_atom(H, mk_concat(hd, tl)));
             conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(hd), i));
-            conclusion_terms.push_back(ctx.mk_eq_atom(e, mk_indexof(tl, N)));
+            conclusion_terms.push_back(u.str.mk_contains(tl, N));
+            conclusion_terms.push_back(ctx.mk_eq_atom(e, m_autil.mk_add(i, mk_indexof(tl, N))));
 
             expr_ref conclusion(mk_and(conclusion_terms), m);
             assert_implication(premise, conclusion);
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 0967c6cc6..6af668506 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -282,6 +282,7 @@ void int_solver::find_feasible_solution() {
 lia_move int_solver::run_gcd_test() {
     if (settings().m_int_run_gcd_test) {
         settings().st().m_gcd_calls++;
+        TRACE("int_solver", tout << "gcd-test " << settings().st().m_gcd_calls << "\n";);
         if (!gcd_test()) {
             settings().st().m_gcd_conflicts++;
             return lia_move::conflict;
@@ -291,6 +292,7 @@ lia_move int_solver::run_gcd_test() {
 }
 
 lia_move int_solver::gomory_cut() {
+    TRACE("int_solver", tout << "gomory " << m_number_of_calls << "\n";);
     if ((m_number_of_calls) % settings().m_int_gomory_cut_period != 0)
         return lia_move::undef;
 
@@ -1052,7 +1054,7 @@ lia_move int_solver::create_branch_on_column(int j) {
         m_k = m_upper? floor(get_value(j)) : ceil(get_value(j));        
     }
 
-    TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n";
+    TRACE("int_solver", tout << "branching v" << j << " = " << get_value(j) << "\n";
           display_column(tout, j);
           tout << "k = " << m_k << std::endl;
           );
diff --git a/src/util/lp/lar_core_solver_def.h b/src/util/lp/lar_core_solver_def.h
index b945b0e51..ca7915c7d 100644
--- a/src/util/lp/lar_core_solver_def.h
+++ b/src/util/lp/lar_core_solver_def.h
@@ -265,12 +265,14 @@ unsigned lar_core_solver::get_number_of_non_ints() const {
 }
 
 void lar_core_solver::solve() {
+    TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
     lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
     lp_assert(m_r_solver.inf_set_is_correct());
 	TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.m_inf_set.size() << ", int_infs = " << get_number_of_non_ints() << std::endl;);
 	if (m_r_solver.current_x_is_feasible() && m_r_solver.m_look_for_feasible_solution_only) {
-		m_r_solver.set_status(lp_status::OPTIMAL);
-		return;
+            m_r_solver.set_status(lp_status::OPTIMAL);
+            TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
+            return;
 	}
     ++settings().st().m_need_to_solve_inf;
     CASSERT("A_off", !m_r_solver.A_mult_x_is_off());
@@ -310,6 +312,8 @@ void lar_core_solver::solve() {
     lp_assert(r_basis_is_OK());
     lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
     lp_assert(m_r_solver.inf_set_is_correct());
+
+    TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
 }
 
 
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 31e9d2654..48b08a215 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -85,6 +85,15 @@ std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostr
     out << "end of implied bound" << std::endl;
     return out;
 }
+
+std::ostream& lar_solver::print_values(std::ostream& out) const {
+    for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
+        const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i];
+        out << this->get_column_name(i) << " -> " << rp << "\n";
+    }
+    return out;
+}
+
     
 bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, const vector<std::pair<mpq, unsigned>> & explanation) const {
     std::unordered_map<unsigned, mpq> coeff_map;
@@ -337,13 +346,12 @@ void lar_solver::shrink_inf_set_after_pop(unsigned n, int_set & set) {
 
     
 void lar_solver::pop(unsigned k) {
-    TRACE("arith_int", tout << "pop" << std::endl;);
+    TRACE("int_solver", tout << "pop" << std::endl;);
     TRACE("lar_solver", tout << "k = " << k << std::endl;);
 
     m_infeasible_column_index.pop(k);
     unsigned n = m_columns_to_ul_pairs.peek_size(k);
     m_var_register.shrink(n);
-    TRACE("arith_int", tout << "pop" << std::endl;);
     if (m_settings.use_tableau()) {
         pop_tableau();
     }
@@ -395,12 +403,15 @@ bool lar_solver::maximize_term_on_tableau(const lar_term & term,
 
     m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::FEASIBLE);
     m_mpq_lar_core_solver.solve();
-    if (m_mpq_lar_core_solver.m_r_solver.get_status() == lp_status::UNBOUNDED)
+    lp_status st = m_mpq_lar_core_solver.m_r_solver.get_status();
+    TRACE("lar_solver", tout << st << "\n";);
+    if (st == lp_status::UNBOUNDED) {
         return false;
-
-    term_max = term.apply(m_mpq_lar_core_solver.m_r_x);
-
-    return true;
+    }
+    else {
+        term_max = term.apply(m_mpq_lar_core_solver.m_r_x);        
+        return true;
+    }
 }
 
 bool lar_solver::costs_are_zeros_for_r_solver() const {
@@ -444,6 +455,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) {
 
 void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
         
+    TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";);
     auto & rslv = m_mpq_lar_core_solver.m_r_solver;
     rslv.m_using_infeas_costs = false;
     lp_assert(costs_are_zeros_for_r_solver());
@@ -463,29 +475,29 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
 bool lar_solver::maximize_term_on_corrected_r_solver(lar_term & term,
                                                      impq &term_max) {
     settings().backup_costs = false;
+    bool ret = false;
+    TRACE("lar_solver", print_term(term, tout << "maximize: ") << "\n"; print_constraints(tout););
     switch (settings().simplex_strategy()) {
     case simplex_strategy_enum::tableau_rows:
         prepare_costs_for_r_solver(term);
         settings().simplex_strategy() = simplex_strategy_enum::tableau_costs;
-        {
-            bool ret = maximize_term_on_tableau(term, term_max);
-            settings().simplex_strategy() = simplex_strategy_enum::tableau_rows;
-            set_costs_to_zero(term);
-            m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
-            return ret;
-        }
+        ret = maximize_term_on_tableau(term, term_max);
+        settings().simplex_strategy() = simplex_strategy_enum::tableau_rows;
+        set_costs_to_zero(term);
+        m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
+        return ret;
+        
     case simplex_strategy_enum::tableau_costs:
         prepare_costs_for_r_solver(term);
-        {
-            bool ret = maximize_term_on_tableau(term, term_max);
-            set_costs_to_zero(term);
-            m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
-            return ret;
-        }
-            
+        ret = maximize_term_on_tableau(term, term_max);
+        set_costs_to_zero(term);
+        m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
+        return ret;
+                    
     case simplex_strategy_enum::lu:
         lp_assert(false); // not implemented
         return false;
+
     default:
         lp_unreachable(); // wrong mode
     }
@@ -497,23 +509,24 @@ bool lar_solver::remove_from_basis(unsigned j) {
     return m_mpq_lar_core_solver.m_r_solver.remove_from_basis(j);
 }
 
-lar_term lar_solver::get_term_to_maximize(unsigned ext_j) const {
-    unsigned local_j;
-    if (m_var_register.external_is_used(ext_j, local_j)) {
-        lar_term r;
-        r. add_monomial(one_of_type<mpq>(), local_j);
-        return r;
+lar_term lar_solver::get_term_to_maximize(unsigned j_or_term) const {
+    if (is_term(j_or_term)) {
+        return get_term(j_or_term);
     }
-    if (!is_term(ext_j) || adjust_term_index(ext_j) >= m_terms.size())
-        return lar_term(); // return an empty term
-    return get_term(ext_j);
+    if (j_or_term < m_mpq_lar_core_solver.m_r_x.size()) {
+        lar_term r;
+        r.add_monomial(one_of_type<mpq>(), j_or_term);
+        return r;
+    } 
+    return lar_term(); // return an empty term
 }
 
-lp_status lar_solver::maximize_term(unsigned ext_j,
+lp_status lar_solver::maximize_term(unsigned j_or_term,
                                impq &term_max) {
+    TRACE("lar_solver", print_values(tout););
     bool was_feasible = m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis();
     impq prev_value;
-    lar_term term = get_term_to_maximize(ext_j);
+    lar_term term = get_term_to_maximize(j_or_term);
     if (term.is_empty()) {
         return lp_status::UNBOUNDED;
     }
@@ -559,7 +572,12 @@ lp_status lar_solver::maximize_term(unsigned ext_j,
         term_max = prev_value;
         m_mpq_lar_core_solver.m_r_x = backup;
     }
-    return term_max == opt_val? lp_status::OPTIMAL :lp_status::FEASIBLE;
+    TRACE("lar_solver", print_values(tout););
+    if (term_max == opt_val) {
+        set_status(lp_status::OPTIMAL);
+        return lp_status::OPTIMAL;
+    }
+    return lp_status::FEASIBLE;
 }
     
 
@@ -945,7 +963,6 @@ bool lar_solver::all_constraints_hold() const {
 }
 
 bool lar_solver::constraint_holds(const lar_base_constraint & constr, std::unordered_map<var_index, mpq> & var_map) const {
-    return true;
     mpq left_side_val = get_left_side_val(constr, var_map);
     switch (constr.m_kind) {
     case LE: return left_side_val <= constr.m_right_side;
@@ -1186,6 +1203,7 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
                 break;
             }
                     
+            TRACE("get_model", tout << get_column_name(i) << " := " << x << "\n";);
             variable_values[i] = x;
         }
     } while (i != m_mpq_lar_core_solver.m_r_x.size());
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 7af9cfacb..39adbd86f 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -310,7 +310,7 @@ public:
                                              impq &term_max);    
     // starting from a given feasible state look for the maximum of the term
     // return true if found and false if unbounded
-    lp_status maximize_term(unsigned ext_j ,
+    lp_status maximize_term(unsigned j_or_term,
                             impq &term_max);
     
 
@@ -457,6 +457,7 @@ public:
 
     std::ostream& print_implied_bound(const implied_bound& be, std::ostream & out) const;
 
+    std::ostream& print_values(std::ostream& out) const;
     
     mpq get_left_side_val(const lar_base_constraint &  cns, const std::unordered_map<var_index, mpq> & var_map) const;
 
diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index 9a6549917..c1b8aa987 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -136,8 +136,6 @@ public:
     }
 
     const vector<unsigned> & non_basis() const { return m_nbasis; }
-
-
     
     void set_status(lp_status status) {
         m_status = status;
diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h
index a43764172..ad861cc7a 100644
--- a/src/util/lp/lp_primal_core_solver_def.h
+++ b/src/util/lp/lp_primal_core_solver_def.h
@@ -357,20 +357,20 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>::try_jump_to_
                                                                                                           bool & unlimited) {
     switch(this->m_column_types[entering]){
     case column_type::boxed: 
-            if (m_sign_of_entering_delta > 0) {
-                t = this->m_upper_bounds[entering] - this->m_x[entering];
-                if (unlimited || t <= theta){
-                    lp_assert(t >= zero_of_type<X>());
-                    return true;
-                }
-            } else { // m_sign_of_entering_delta == -1
-                t = this->m_x[entering] - this->m_lower_bounds[entering];
-                if (unlimited || t <= theta) {
-                    lp_assert(t >= zero_of_type<X>());
-                    return true;
-                }
+        if (m_sign_of_entering_delta > 0) {
+            t = this->m_upper_bounds[entering] - this->m_x[entering];
+            if (unlimited || t <= theta){
+                lp_assert(t >= zero_of_type<X>());
+                return true;
             }
-            return false;
+        } else { // m_sign_of_entering_delta == -1
+            t = this->m_x[entering] - this->m_lower_bounds[entering];
+            if (unlimited || t <= theta) {
+                lp_assert(t >= zero_of_type<X>());
+                return true;
+            }
+        }
+        return false;
     case column_type::upper_bound:
         if (m_sign_of_entering_delta > 0) {
             t = this->m_upper_bounds[entering] - this->m_x[entering];
@@ -775,6 +775,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
     X t;
     int leaving = find_leaving_and_t_precise(entering, t);
     if (leaving == -1) {
+        TRACE("lar_solver", tout << "non-leaving\n";);
         this->set_status(lp_status::UNBOUNDED);
         return;
     }
@@ -828,6 +829,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
         } else {
             this->set_status(lp_status::TENTATIVE_UNBOUNDED);
         }
+        TRACE("lar_solver", tout << this->get_status() << "\n";);
         return;
     }
     advance_on_entering_and_leaving(entering, leaving, t);
@@ -857,8 +859,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column
         out << this->m_column_norms[j] << " ";
     }
     out << std::endl;
-    out << std::endl;
-}
+ }
 
 // returns the number of iterations
 template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve() {
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 6776acf65..178d5042d 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -1784,7 +1784,7 @@ void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) {
 template<bool SYNCH>
 void mpz_manager<SYNCH>::display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const {
     if (is_small(a)) {
-        display_binary_data(out, get_uint64(a), num_bits);
+        display_binary_data(out, static_cast<unsigned>(get_uint64(a)), num_bits);
     } else {
 #ifndef _MP_GMP
         digit_t *ds = digits(a);
diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h
index 1135c893e..da1a3deaa 100644
--- a/src/util/stopwatch.h
+++ b/src/util/stopwatch.h
@@ -60,7 +60,7 @@ public:
     }
 
     void stop() {
-        SASSERT(m_running);
+        // SASSERT(m_running);
         DEBUG_CODE(m_running = false;);
         m_elapsed += get() - m_start;
     }