diff --git a/scripts/update_api.py b/scripts/update_api.py
index b082c96e1..22c0dea99 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1665,6 +1665,7 @@ for v in ('Z3_LIBRARY_PATH', 'PATH', 'PYTHONPATH'):
 
 _all_dirs.extend(_default_dirs)
 
+_failures = []
 for d in _all_dirs:
   try:
     d = os.path.realpath(d)
@@ -1673,14 +1674,16 @@ for d in _all_dirs:
       if os.path.isfile(d):
         _lib = ctypes.CDLL(d)
         break
-  except:
+  except Exception as e:
+    _failures += [e]
     pass
 
 if _lib is None:
   # If all else failed, ask the system to find it.
   try:
     _lib = ctypes.CDLL('libz3.%s' % _ext)
-  except:
+  except Exception as e:
+    _failures += [e]
     pass
 
 if _lib is None:
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 5828b0fcd..4f4da6bd4 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -384,12 +384,14 @@ extern "C" {
     Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d) {
         LOG_Z3_get_decl_name(c, d);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, nullptr);
         return of_symbol(to_func_decl(d)->get_name());
     }
 
     unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d) {
         LOG_Z3_get_decl_num_parameters(c, d);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, 0);
         return to_func_decl(d)->get_num_parameters();
     }
 
@@ -397,6 +399,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_decl_parameter_kind(c, d, idx);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, Z3_PARAMETER_INT);
         if (idx >= to_func_decl(d)->get_num_parameters()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return Z3_PARAMETER_INT;
@@ -429,6 +432,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_decl_int_parameter(c, d, idx);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, 0);
         if (idx >= to_func_decl(d)->get_num_parameters()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return 0;
@@ -446,6 +450,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_decl_double_parameter(c, d, idx);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, 0);
         if (idx >= to_func_decl(d)->get_num_parameters()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return 0;
@@ -463,6 +468,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_decl_symbol_parameter(c, d, idx);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, 0);
         if (idx >= to_func_decl(d)->get_num_parameters()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return nullptr;
@@ -480,6 +486,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_decl_sort_parameter(c, d, idx);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, 0);
         if (idx >= to_func_decl(d)->get_num_parameters()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             RETURN_Z3(nullptr);
@@ -497,6 +504,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_decl_ast_parameter(c, d, idx);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, 0);
         if (idx >= to_func_decl(d)->get_num_parameters()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             RETURN_Z3(nullptr);
@@ -514,6 +522,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_decl_func_decl_parameter(c, d, idx);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, 0);
         if (idx >= to_func_decl(d)->get_num_parameters()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             RETURN_Z3(nullptr);
@@ -531,6 +540,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_decl_rational_parameter(c, d, idx);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, "");
         if (idx >= to_func_decl(d)->get_num_parameters()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return "";
@@ -549,6 +559,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_sort_name(c, t);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(t, nullptr);
         return of_symbol(to_sort(t)->get_name());
         Z3_CATCH_RETURN(nullptr);
     }
@@ -567,6 +578,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_arity(c, d);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, 0);
         return to_func_decl(d)->get_arity();
         Z3_CATCH_RETURN(0);
     }
@@ -575,6 +587,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_domain_size(c, d);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, 0);
         return to_func_decl(d)->get_arity();
         Z3_CATCH_RETURN(0);
     }
@@ -583,6 +596,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_domain(c, d, i);
         RESET_ERROR_CODE();
+        CHECK_VALID_AST(d, 0);
         if (i >= to_func_decl(d)->get_arity()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             RETURN_Z3(nullptr);
diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index b5458cff2..2b77294d5 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include "ast/fpa_decl_plugin.h"
 
 bool is_numeral_sort(Z3_context c, Z3_sort ty) {
+    if (!ty) return false;
     sort * _ty = to_sort(ty);
     family_id fid  = _ty->get_family_id();
     if (fid != mk_c(c)->get_arith_fid() &&
@@ -145,7 +146,8 @@ extern "C" {
     Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a) {
         Z3_TRY;
         LOG_Z3_is_numeral_ast(c, a);
-        RESET_ERROR_CODE();
+        RESET_ERROR_CODE();        
+        CHECK_IS_EXPR(a, Z3_FALSE);
         expr* e = to_expr(a);
         return
             mk_c(c)->autil().is_numeral(e) ||
@@ -160,11 +162,8 @@ extern "C" {
         Z3_TRY;
         // This function is not part of the public API
         RESET_ERROR_CODE();
+        CHECK_IS_EXPR(a, Z3_FALSE);
         expr* e = to_expr(a);
-        if (!e) {
-            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return Z3_FALSE;
-        }
         if (mk_c(c)->autil().is_numeral(e, r)) {
             return Z3_TRUE;
         }
@@ -187,6 +186,7 @@ extern "C" {
         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_string(c, a);
         RESET_ERROR_CODE();
+        CHECK_IS_EXPR(a, "");
         rational r;
         Z3_bool ok = Z3_get_numeral_rational(c, a, r);
         if (ok == Z3_TRUE) {
@@ -232,11 +232,8 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_numeral_decimal_string(c, a, precision);
         RESET_ERROR_CODE();
+        CHECK_IS_EXPR(a, "");
         expr* e = to_expr(a);
-        if (!e) {
-            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return "";
-        }
         rational r;
         arith_util & u = mk_c(c)->autil();
         if (u.is_numeral(e, r) && !r.is_int()) {
@@ -267,6 +264,7 @@ extern "C" {
         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_small(c, a, num, den);
         RESET_ERROR_CODE();
+        CHECK_IS_EXPR(a, Z3_FALSE);
         rational r;
         Z3_bool ok = Z3_get_numeral_rational(c, a, r);
         if (ok == Z3_TRUE) {
@@ -292,6 +290,7 @@ extern "C" {
         // This function invokes Z3_get_numeral_int64, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_int(c, v, i);
         RESET_ERROR_CODE();
+        CHECK_IS_EXPR(v, Z3_FALSE);
         if (!i) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             return Z3_FALSE;
@@ -310,6 +309,7 @@ extern "C" {
         // This function invokes Z3_get_numeral_uint64, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_uint(c, v, u);
         RESET_ERROR_CODE();
+        CHECK_IS_EXPR(v, Z3_FALSE);
         if (!u) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             return Z3_FALSE;
@@ -328,6 +328,7 @@ extern "C" {
         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_uint64(c, v, u);
         RESET_ERROR_CODE();
+        CHECK_IS_EXPR(v, Z3_FALSE);
         if (!u) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             return Z3_FALSE;
@@ -348,6 +349,7 @@ extern "C" {
         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_int64(c, v, i);
         RESET_ERROR_CODE();
+        CHECK_IS_EXPR(v, Z3_FALSE);
         if (!i) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             return Z3_FALSE;
@@ -367,6 +369,7 @@ extern "C" {
         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_rational_int64(c, v, num, den);
         RESET_ERROR_CODE();
+        CHECK_IS_EXPR(v, Z3_FALSE);
         if (!num || !den) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             return Z3_FALSE;
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 7711ec4cd..0eeeeaecc 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -1675,7 +1675,6 @@ def Or(*args):
 class PatternRef(ExprRef):
     """Patterns are hints for quantifier instantiation.
 
-    See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
     """
     def as_ast(self):
         return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
@@ -1686,8 +1685,6 @@ class PatternRef(ExprRef):
 def is_pattern(a):
     """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
 
-    See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
-
     >>> f = Function('f', IntSort(), IntSort())
     >>> x = Int('x')
     >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
@@ -1705,8 +1702,6 @@ def is_pattern(a):
 def MultiPattern(*args):
     """Create a Z3 multi-pattern using the given expressions `*args`
 
-    See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
-
     >>> f = Function('f', IntSort(), IntSort())
     >>> g = Function('g', IntSort(), IntSort())
     >>> x = Int('x')
@@ -1966,8 +1961,6 @@ def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
 
     The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
 
-    See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
-
     >>> f = Function('f', IntSort(), IntSort(), IntSort())
     >>> x = Int('x')
     >>> y = Int('y')
@@ -1985,7 +1978,6 @@ def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
 
     The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
 
-    See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
 
     >>> f = Function('f', IntSort(), IntSort(), IntSort())
     >>> x = Int('x')
diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index be3a02019..3c5e2e1c0 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -351,6 +351,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
     case OP_MUL:     return is_real ? m_r_mul_decl : m_i_mul_decl;
     case OP_DIV:     return m_r_div_decl;
     case OP_IDIV:    return m_i_div_decl;
+    case OP_IDIVIDES: UNREACHABLE(); 
     case OP_REM:     return m_i_rem_decl;
     case OP_MOD:     return m_i_mod_decl;
     case OP_TO_REAL: return m_to_real_decl;
@@ -482,6 +483,14 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         m_manager->raise_exception("no arguments supplied to arithmetical operator");
         return nullptr;
     }
+    if (k == OP_IDIVIDES) {
+        if (arity != 1 || domain[0] != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) {
+            m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer");
+        }
+        return m_manager->mk_func_decl(symbol("divides"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
+                                       func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
+
     if (m_manager->int_real_coercions() && use_coercion(k)) {
         return mk_func_decl(fix_kind(k, arity), has_real_arg(arity, domain, m_real_decl));
     }
@@ -499,6 +508,13 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         m_manager->raise_exception("no arguments supplied to arithmetical operator");
         return nullptr;
     }
+    if (k == OP_IDIVIDES) {
+        if (num_args != 1 || m_manager->get_sort(args[0]) != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) {
+            m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer");
+        }
+        return m_manager->mk_func_decl(symbol("divides"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
+                                       func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
     if (m_manager->int_real_coercions() && use_coercion(k)) {
         return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl));
     }
@@ -533,6 +549,7 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
     op_names.push_back(builtin_name("*",OP_MUL));
     op_names.push_back(builtin_name("/",OP_DIV));
     op_names.push_back(builtin_name("div",OP_IDIV));
+    op_names.push_back(builtin_name("divides",OP_IDIVIDES));
     op_names.push_back(builtin_name("rem",OP_REM));
     op_names.push_back(builtin_name("mod",OP_MOD));
     op_names.push_back(builtin_name("to_real",OP_TO_REAL));
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index f5f82b5fd..09f082522 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -46,6 +46,7 @@ enum arith_op_kind {
     OP_MUL,
     OP_DIV,
     OP_IDIV,
+    OP_IDIVIDES,
     OP_REM,
     OP_MOD,
     OP_TO_REAL,
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index a927df3b5..5fcc8d63b 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2369,6 +2369,15 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector<expr> &args) {
     return true;
 }
 
+static void trace_quant(std::ostream& strm, quantifier* q) {
+    strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]")
+         << " #" << q->get_id() << " " << q->get_qid();
+    for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
+        strm << " #" << q->get_pattern(i)->get_id();
+    }
+    strm << " #" << q->get_expr()->get_id() << "\n";
+}
+
 
 quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names,
                                         expr * body, int weight , symbol const & qid, symbol const & skid,
@@ -2401,12 +2410,7 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s
     quantifier * r = register_node(new_node);
 
     if (m_trace_stream && r == new_node) {
-        *m_trace_stream << "[mk-quant] #" << r->get_id() << " " << qid;
-        for (unsigned i = 0; i < num_patterns; ++i) {
-            *m_trace_stream << " #" << patterns[i]->get_id();
-        }
-        *m_trace_stream << " #" << body->get_id() << "\n";
-
+        trace_quant(*m_trace_stream, r);
     }
 
     return r;
@@ -2420,6 +2424,9 @@ quantifier * ast_manager::mk_lambda(unsigned num_decls, sort * const * decl_sort
     sort* s = autil.mk_array_sort(num_decls, decl_sorts, ::get_sort(body));
     quantifier * new_node = new (mem) quantifier(num_decls, decl_sorts, decl_names, body, s);
     quantifier * r = register_node(new_node);
+    if (m_trace_stream && r == new_node) {
+        trace_quant(*m_trace_stream, r);
+    }
     return r;
 }
 
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 8035254b4..72ce9c761 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -66,6 +66,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
         SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break;
     case OP_IDIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
         SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break;
+    case OP_IDIVIDES: SASSERT(num_args == 1); st = mk_idivides(f->get_parameter(0).get_int(), args[0], result); break;
     case OP_MOD: SASSERT(num_args == 2); st = mk_mod_core(args[0], args[1], result); break;
     case OP_REM: SASSERT(num_args == 2); st = mk_rem_core(args[0], args[1], result); break;
     case OP_UMINUS: SASSERT(num_args == 1);  st = mk_uminus(args[0], result); break;
@@ -792,6 +793,11 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul
     return BR_FAILED;
 }
 
+br_status arith_rewriter::mk_idivides(unsigned k, expr * arg, expr_ref & result) {
+    result = m().mk_eq(m_util.mk_mod(arg, m_util.mk_int(k)), m_util.mk_int(0));
+    return BR_REWRITE2;
+}
+
 br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result) {
     set_curr_sort(m().get_sort(arg1));
     numeral v1, v2;
diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h
index 93b6e5ad5..dd7623a9b 100644
--- a/src/ast/rewriter/arith_rewriter.h
+++ b/src/ast/rewriter/arith_rewriter.h
@@ -143,6 +143,7 @@ public:
 
     br_status mk_div_core(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_idivides(unsigned k, expr * arg, expr_ref & result);
     br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_rem_core(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_power_core(expr* arg1, expr* arg2, expr_ref & result);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index af5ef3b0b..84c05d53e 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1866,6 +1866,52 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
     }
 }
 
+bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) {
+    m_lhs.reset();
+    m_util.str.get_concat(a, m_lhs);
+    TRACE("seq", tout << expr_ref(a, m()) << " " << expr_ref(b, m()) << "\n";);
+    zstring s;
+    for (unsigned i = 0; i < m_lhs.size(); ++i) {
+        expr* e = m_lhs.get(i);
+        if (m_util.str.is_empty(e)) {
+            continue;
+        }
+
+        if (m_util.str.is_string(e, s)) {
+            unsigned sz = s.length();
+            expr_ref_vector es(m());
+            for (unsigned j = 0; j < sz; ++j) {
+                es.push_back(m_util.str.mk_unit(m_util.str.mk_char(s, j)));
+            }
+            es.append(m_lhs.size() - i, m_lhs.c_ptr() + i);
+            for (unsigned j = 0; j < sz; ++j) {
+                disj.push_back(m_util.str.mk_prefix(b, m_util.str.mk_concat(es.size() - j, es.c_ptr() + j)));
+            }
+            continue;
+        }
+        if (m_util.str.is_unit(e)) {
+            disj.push_back(m_util.str.mk_prefix(b, m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i)));
+            continue;
+        }
+
+        if (m_util.str.is_string(b, s)) {
+            expr* all = m_util.re.mk_full_seq(m_util.re.mk_re(m().get_sort(b)));
+            disj.push_back(m_util.re.mk_in_re(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i),
+                                              m_util.re.mk_concat(all, m_util.re.mk_concat(m_util.re.mk_to_re(b), all))));
+            return true;
+        }
+
+        if (i == 0) {
+            return false;
+        }
+        disj.push_back(m_util.str.mk_contains(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i), b));
+        return true;
+    }
+    disj.push_back(m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b))));
+    return true;
+}
+
+
 expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
     SASSERT(n > 0);
     ptr_vector<expr> bs;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index c96096c65..f5878b2c2 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -168,6 +168,8 @@ public:
 
     bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);
 
+    bool reduce_contains(expr* a, expr* b, expr_ref_vector& disj);
+
     void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& lhs, expr_ref_vector& rhs);
 
 
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 585dd0fa6..be3acc261 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1063,7 +1063,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
         return;
     }
     if (num_indices > 0)
-        throw cmd_exception("invalid use of indexed indentifier, unknown builtin function ", s);
+        throw cmd_exception("invalid use of indexed identifier, unknown builtin function ", s);
     expr* _t;
     if (macros_find(s, num_args, args, _t)) {
         TRACE("macro_bug", tout << "well_sorted_check_enabled(): " << well_sorted_check_enabled() << "\n";
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 566aaa1f6..e5c0bcddb 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1012,8 +1012,7 @@ namespace opt {
             }
         }
         // fix types of objectives:
-        for (unsigned i = 0; i < m_objectives.size(); ++i) {
-            objective & obj = m_objectives[i];
+        for (objective & obj : m_objectives) {
             expr* t = obj.m_term;
             switch(obj.m_type) {
             case O_MINIMIZE:
@@ -1189,13 +1188,12 @@ namespace opt {
     void context::update_bound(bool is_lower) {
         expr_ref val(m);
         if (!m_model.get()) return;
-        for (unsigned i = 0; i < m_objectives.size(); ++i) {
-            objective const& obj = m_objectives[i];
+        for (objective const& obj : m_objectives) {
             rational r;
             switch(obj.m_type) {
             case O_MINIMIZE: {
                 val = (*m_model)(obj.m_term);
-                TRACE("opt", tout << obj.m_term << " " << val << " " << is_numeral(val, r) << "\n";);
+                TRACE("opt", tout << obj.m_term << " " << val << "\n";);
                 if (is_numeral(val, r)) {
                     inf_eps val = inf_eps(obj.m_adjust_value(r));
                     TRACE("opt", tout << "adjusted value: " << val << "\n";);
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index c71a6e21d..00e079989 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -401,7 +401,7 @@ namespace smt {
         label_hasher &             m_lbl_hasher;
         func_decl *                m_root_lbl;
         unsigned                   m_num_args; //!< we need this information to avoid the nary *,+ crash bug
-        unsigned char              m_filter_candidates;
+        bool                       m_filter_candidates;
         unsigned                   m_num_regs;
         unsigned                   m_num_choices;
         instruction *              m_root;
@@ -531,7 +531,7 @@ namespace smt {
         }
 
         bool filter_candidates() const {
-            return m_filter_candidates != 0;
+            return m_filter_candidates;
         }
 
         const instruction * get_root() const {
@@ -1978,10 +1978,10 @@ namespace smt {
 #define INIT_ARGS_SIZE 16
 
     public:
-        interpreter(context & ctx, mam & m, bool use_filters):
+        interpreter(context & ctx, mam & ma, bool use_filters):
             m_context(ctx),
             m_ast_manager(ctx.get_manager()),
-            m_mam(m),
+            m_mam(ma),
             m_use_filters(use_filters) {
             m_args.resize(INIT_ARGS_SIZE);
         }
@@ -2002,6 +2002,7 @@ namespace smt {
             init(t);
             if (t->filter_candidates()) {
                 for (enode* app : t->get_candidates()) {
+                    TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
                     if (!app->is_marked() && app->is_cgr()) {
                         if (m_context.resource_limits_exceeded() || !execute_core(t, app))
                             return;
@@ -2837,7 +2838,7 @@ namespace smt {
             mk_tree_trail(ptr_vector<code_tree> & t, unsigned id):m_trees(t), m_lbl_id(id) {}
             void undo(mam_impl & m) override {
                 dealloc(m_trees[m_lbl_id]);
-                m_trees[m_lbl_id] = 0;
+                m_trees[m_lbl_id] = nullptr;
             }
         };
 
@@ -2870,8 +2871,8 @@ namespace smt {
             app * p           = to_app(mp->get_arg(first_idx));
             func_decl * lbl   = p->get_decl();
             unsigned lbl_id   = lbl->get_decl_id();
-            m_trees.reserve(lbl_id+1, 0);
-            if (m_trees[lbl_id] == 0) {
+            m_trees.reserve(lbl_id+1, nullptr);
+            if (m_trees[lbl_id] == nullptr) {
                 m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false);
                 SASSERT(m_trees[lbl_id]->expected_num_args() == p->get_num_args());
                 DEBUG_CODE(m_trees[lbl_id]->set_context(m_context););
@@ -2956,7 +2957,7 @@ namespace smt {
             m_ground_arg(ground_arg),
             m_pattern_idx(pat_idx),
             m_child(child) {
-            SASSERT(ground_arg != 0 || ground_arg_idx == 0);
+            SASSERT(ground_arg != nullptr || ground_arg_idx == 0);
         }
     };
 
@@ -3223,7 +3224,7 @@ namespace smt {
 
         path_tree * mk_path_tree(path * p, quantifier * qa, app * mp) {
             SASSERT(m_ast_manager.is_pattern(mp));
-            SASSERT(p != 0);
+            SASSERT(p != nullptr);
             unsigned pat_idx = p->m_pattern_idx;
             path_tree * head = nullptr;
             path_tree * curr = nullptr;
@@ -3516,9 +3517,7 @@ namespace smt {
                     std::cout << "Avg. " << static_cast<double>(total_sz)/static_cast<double>(counter) << ", Max. " << max_sz << "\n";
 #endif
 
-                enode_vector::iterator it1  = v->begin();
-                enode_vector::iterator end1 = v->end();
-                for (; it1 != end1; ++it1) {
+                for (enode* n : *v) {
                     // Two different kinds of mark are used:
                     // - enode mark field:  it is used to mark the already processed parents.
                     // - enode mark2 field: it is used to mark the roots already added to be processed in the next level.
@@ -3527,7 +3526,7 @@ namespace smt {
                     // and Z3 may fail to find potential new matches.
                     //
                     // The file regression\acu.sx exposed this problem.
-                    enode * curr_child = (*it1)->get_root();
+                    enode * curr_child = n->get_root();
 
                     if (m_use_filters && curr_child->get_plbls().empty_intersection(filter))
                         continue;
@@ -3591,7 +3590,7 @@ namespace smt {
                                          is_eq(curr_tree->m_ground_arg, curr_parent->get_arg(curr_tree->m_ground_arg_idx))
                                          )) {
                                         if (curr_tree->m_code) {
-                                            TRACE("mam_path_tree", tout << "found candidate\n";);
+                                            TRACE("mam_path_tree", tout << "found candidate " << expr_ref(curr_parent->get_owner(), m_ast_manager) << "\n";);
                                             add_candidate(curr_tree->m_code, curr_parent);
                                         }
                                         if (curr_tree->m_first_child) {
diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp
index da589893b..114f9cf29 100644
--- a/src/smt/old_interval.cpp
+++ b/src/smt/old_interval.cpp
@@ -561,15 +561,24 @@ interval & interval::operator/=(interval const & other) {
         TRACE("interval", other.display_with_dependencies(tout););
         if (other.m_lower.is_pos() || (other.m_lower.is_zero() && other.m_lower_open)) {
             // other.lower > 0
+            //     x in ([0, 0] / [other.lo, other.up]), for other.lo > 0
+            // <=>
+            //     x >= 0: because y*x >= 0 & y > 0
+            //     x <= 0: because y*x <= 0 & y > 0
             m_lower_dep  = join(m_lower_dep, other.m_lower_dep);
             m_upper_dep  = join(m_upper_dep, other.m_lower_dep);
         }
         else {
             // assertion must hold since !other.contains_zero()
-            SASSERT(other.m_upper.is_neg() || (other.m_upper.is_zero() && other.m_upper_open));
+            SASSERT(other.m_upper.is_neg() || (other.m_upper.is_zero() && other.m_upper_open));            
             // other.upper < 0
-            m_lower_dep  = join(m_lower_dep, other.m_upper_dep);
-            m_upper_dep  = join(m_upper_dep, other.m_upper_dep);
+            //     x in ([0, 0] / [other.lo, other.up]), for up < 0
+            // <=>
+            //     x >= 0: because y*x <= 0 & y < 0
+            //     x <= 0: because y*x >= 0 & y < 0
+            v_dependency* lower_dep = m_lower_dep;
+            m_lower_dep  = join(m_upper_dep, other.m_upper_dep);
+            m_upper_dep  = join(lower_dep, other.m_upper_dep);
         }
         return *this;
     }
diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h
index 9d09b4c38..fe7cc6060 100644
--- a/src/smt/params/theory_arith_params.h
+++ b/src/smt/params/theory_arith_params.h
@@ -19,7 +19,7 @@ Revision History:
 #ifndef THEORY_ARITH_PARAMS_H_
 #define THEORY_ARITH_PARAMS_H_
 
-#include<limits.h>
+#include<climits>
 #include "util/params.h"
 
 enum arith_solver_id {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 44147c668..6216d6592 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -228,7 +228,6 @@ namespace smt {
     }
 
     void context::copy_plugins(context& src, context& dst) {
-
         // copy theory plugins
         for (theory* old_th : src.m_theory_set) {
             theory * new_th = old_th->mk_fresh(&dst);
@@ -236,8 +235,8 @@ namespace smt {
         }
     }
 
-    context * context::mk_fresh(symbol const * l, smt_params * p) {
-        context * new_ctx = alloc(context, m_manager, p == nullptr ? m_fparams : *p);
+    context * context::mk_fresh(symbol const * l, smt_params * p, params_ref const& pa) {
+        context * new_ctx = alloc(context, m_manager, p ? *p : m_fparams, pa);
         new_ctx->set_logic(l == nullptr ? m_setup.get_logic() : *l);
         copy_plugins(*this, *new_ctx);
         return new_ctx;
@@ -1351,18 +1350,9 @@ namespace smt {
        \remark The method assign_eq adds a new entry on this queue.
     */
     bool context::propagate_eqs() {
-        for (unsigned i = 0; i < m_eq_propagation_queue.size(); i++) {
+        TRACE("add_eq", tout << m_eq_propagation_queue.size() << "\n";);
+        for (unsigned i = 0; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) {
             new_eq & entry = m_eq_propagation_queue[i];
-#if 0
-            static unsigned counter1 = 0;
-            static unsigned counter2 = 0;
-            if (entry.m_lhs->is_eq() || entry.m_rhs->is_eq())
-                counter1++;
-            else
-                counter2++;
-            if ((counter1 + counter2) % 10000 == 0)
-                std::cout << counter1 << " " << counter2 << "\n";
-#endif
             add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification);
             if (inconsistent())
                 return false;
@@ -1376,7 +1366,7 @@ namespace smt {
     */
     bool context::propagate_atoms() {
         SASSERT(!inconsistent());
-        for (unsigned i = 0; i < m_atom_propagation_queue.size(); i++) {
+        for (unsigned i = 0; i < m_atom_propagation_queue.size() && !get_cancel_flag(); i++) {
             SASSERT(!inconsistent());
             literal  l = m_atom_propagation_queue[i];
             bool_var v = l.var();
@@ -1558,16 +1548,17 @@ namespace smt {
     lbool context::get_assignment(expr * n) const {
         if (m_manager.is_false(n))
             return l_false;
-        if (m_manager.is_not(n))
-            return ~get_assignment_core(to_app(n)->get_arg(0));
+        expr* arg = nullptr;
+        if (m_manager.is_not(n, arg))
+            return ~get_assignment_core(arg);
         return get_assignment_core(n);
     }
 
     lbool context::find_assignment(expr * n) const {
         if (m_manager.is_false(n))
             return l_false;
-        if (m_manager.is_not(n)) {
-            expr * arg = to_app(n)->get_arg(0);
+        expr* arg = nullptr;
+        if (m_manager.is_not(n, arg)) {
             if (b_internalized(arg))
                 return ~get_assignment_core(arg);
             return l_undef;
@@ -1752,6 +1743,10 @@ namespace smt {
                 return false;
             if (!propagate_eqs())
                 return false;
+            if (get_cancel_flag()) {
+                m_qhead = qhead;
+                return true;
+            }
             propagate_th_eqs();
             propagate_th_diseqs();
             if (inconsistent())
@@ -3264,6 +3259,7 @@ namespace smt {
     }
 
     void context::reset_assumptions() {
+        TRACE("unsat_core_bug", tout << "reset " << m_assumptions << "\n";);
         for (literal lit : m_assumptions) 
             get_bdata(lit.var()).m_assumption = false;
         m_assumptions.reset();
@@ -4106,9 +4102,7 @@ namespace smt {
         }
 
         SASSERT(!inconsistent());
-        unsigned sz = m_b_internalized_stack.size();
-        for (unsigned i = 0; i < sz; i++) {
-            expr * curr = m_b_internalized_stack.get(i);
+        for (expr * curr : m_b_internalized_stack) { 
             if (is_relevant(curr) && get_assignment(curr) == l_true) {
                 // if curr is a label literal, then its tags will be copied to result.
                 m_manager.is_label_lit(curr, result);
@@ -4124,9 +4118,7 @@ namespace smt {
     void context::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
         SASSERT(!inconsistent());
         buffer<symbol> lbls;
-        unsigned sz = m_b_internalized_stack.size();
-        for (unsigned i = 0; i < sz; i++) {
-            expr * curr = m_b_internalized_stack.get(i);
+        for (expr * curr : m_b_internalized_stack) {
             if (is_relevant(curr) && get_assignment(curr) == l_true) {
                 lbls.reset();
                 if (m_manager.is_label_lit(curr, lbls)) {
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 2ac5695b3..ff92f6f95 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -491,7 +491,7 @@ namespace smt {
         }
 
         bool tracking_assumptions() const {
-            return m_search_lvl > m_base_lvl;
+            return !m_assumptions.empty() && m_search_lvl > m_base_lvl;
         }
 
         expr * bool_var2expr(bool_var v) const {
@@ -1011,6 +1011,7 @@ namespace smt {
 
         void push_eq(enode * lhs, enode * rhs, eq_justification const & js) {
             SASSERT(lhs != rhs);
+            SASSERT(lhs->get_root() != rhs->get_root());
             m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js));
         }
 
@@ -1492,7 +1493,7 @@ namespace smt {
            If l == 0, then the logic of this context is used in the new context.
            If p == 0, then this->m_params is used
         */
-        context * mk_fresh(symbol const * l = nullptr,  smt_params * p = nullptr);
+        context * mk_fresh(symbol const * l = nullptr,  smt_params * smtp = nullptr, params_ref const & p = params_ref());
 
         static void copy(context& src, context& dst);
 
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 8a75dc48c..2a46fd07f 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -422,8 +422,6 @@ namespace smt {
         out << "(check-sat)\n";
     }
 
-#define BUFFER_SZ 128
-
     unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
         std::stringstream strm;
         strm << "lemma_" << (++m_lemma_id) << ".smt2";
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index ae023078a..1414cb522 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -678,8 +678,18 @@ namespace smt {
                 push_trail(set_merge_tf_trail(n));
             n->m_merge_tf = true;
             lbool val = get_assignment(v); 
-            if (val != l_undef)
-                push_eq(n, val == l_true ? m_true_enode : m_false_enode, eq_justification(literal(v, val == l_false)));
+            switch (val) {
+            case l_undef: 
+                break;
+            case l_true: 
+                if (n->get_root() != m_true_enode->get_root()) 
+                    push_eq(n, m_true_enode, eq_justification(literal(v, false))); 
+                break;
+            case l_false: 
+                if (n->get_root() != m_false_enode->get_root()) 
+                    push_eq(n, m_false_enode, eq_justification(literal(v, true))); 
+                break;
+            }
         }
     }
 
diff --git a/src/smt/smt_literal.h b/src/smt/smt_literal.h
index 7f554d740..598335cff 100644
--- a/src/smt/smt_literal.h
+++ b/src/smt/smt_literal.h
@@ -103,7 +103,7 @@ namespace smt {
 
     void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map);
 
-    void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = " ");
+    void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = "\n");
 
     template<typename T>
     void neg_literals(unsigned num_lits, literal const * lits, T & result) {
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index f4c5c09d9..0fea4d13d 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -384,10 +384,13 @@ namespace smt {
             m_fparams = alloc(smt_params, m_context->get_fparams());
             m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free
             m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3.
+            m_fparams->m_arith_dump_lemmas = false;
         }
         if (!m_aux_context) {
             symbol logic;
-            m_aux_context = m_context->mk_fresh(&logic, m_fparams.get());
+            params_ref p;
+            p.set_bool("arith.dump_lemmas", false);
+            m_aux_context = m_context->mk_fresh(&logic, m_fparams.get(), p);
         }
     }
 
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 932ca597f..9e38fef69 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -627,9 +627,6 @@ namespace smt {
             m_params.m_phase_selection         = PS_CACHING_CONSERVATIVE2;
             m_params.m_random_initial_activity = IA_ZERO;
         }
-        // if (st.m_num_arith_ineqs == st.m_num_diff_ineqs && st.m_num_arith_eqs == st.m_num_diff_eqs && st.arith_k_sum_is_small()) 
-        //    m_context.register_plugin(new smt::theory_si_arith(m_manager, m_params));
-        // else 
         setup_i_arith();
         setup_arrays();
     }
@@ -654,7 +651,7 @@ namespace smt {
         // 
         m_params.m_ng_lift_ite             = LI_FULL;
         TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";);
-        setup_i_arith();
+        m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
         setup_arrays();
     }
 
@@ -832,7 +829,10 @@ namespace smt {
                 m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
             break;
         case AS_NEW_ARITH:
-            setup_lra_arith();
+            if (st.m_num_non_linear != 0) 
+                m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
+            else 
+                setup_lra_arith();
             break;
         default:
             m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
@@ -994,7 +994,7 @@ namespace smt {
         }
 
         if (st.num_theories() == 2 && st.has_uf() && is_arith(st)) {
-            if (!st.m_has_real)
+            if (!st.m_has_real && st.m_num_non_linear == 0)
                 setup_QF_UFLIA(st);
             else if (!st.m_has_int && st.m_num_non_linear == 0) 
                 setup_QF_UFLRA();
diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index b5ad68adc..63c6d7417 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -123,7 +123,7 @@ namespace smt {
         context & ctx = get_context();
         app * eq = ctx.mk_eq_atom(a, b);
         TRACE("mk_var_bug", tout << "mk_eq: " << eq->get_id() << " " << a->get_id() << " " << b->get_id() << "\n";
-              tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager()););
+              tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager()););		
         ctx.internalize(eq, gate_ctx);
         return ctx.get_literal(eq);
     }
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index daf285a54..9526637e9 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -731,35 +731,34 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
 
+        TRACE("arith", tout << m_lits << " " << m_eqs.size() << "\n";);
         if (proofs_enabled) {
-            for (unsigned i = 0; i < m_lits.size(); ++i) {
-                a.push_lit(m_lits[i], coeff, proofs_enabled);
-            }
-            for (unsigned i = 0; i < m_eqs.size(); ++i) {
-                a.push_eq(m_eqs[i], coeff, proofs_enabled);
-            }
+            for (literal l : m_lits)    
+                a.push_lit(l, coeff, proofs_enabled);
+            for (auto const& e : m_eqs) 
+                a.push_eq(e, coeff, proofs_enabled);
         }
         else {
             a.append(m_lits.size(), m_lits.c_ptr());
-            a.append(m_eqs.size(), m_eqs.c_ptr());
+            a.append(m_eqs.size(),  m_eqs.c_ptr());
         }
     }
 
     template<typename Ext>
     void theory_arith<Ext>::derived_bound::display(theory_arith<Ext> const& th, std::ostream& out) const {
-      out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << bound::get_value();
-        
         ast_manager& m = th.get_manager();
-        for (unsigned i = 0; i < m_eqs.size(); ++i) {
-            enode* a = m_eqs[i].first;
-            enode* b = m_eqs[i].second;
+        out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << bound::get_value() << "\n";
+        out << "expr: " << mk_pp(th.var2expr(bound::get_var()), m) << "\n";
+        
+        for (auto const& e : m_eqs) {
+            enode* a = e.first;
+            enode* b = e.second;
             out << " ";
             out << "#" << a->get_owner_id() << " " << mk_pp(a->get_owner(), m) << " = "
-                << "#" << b->get_owner_id() << " " << mk_pp(b->get_owner(), m);
+                << "#" << b->get_owner_id() << " " << mk_pp(b->get_owner(), m) << "\n";
         }
-        for (unsigned i = 0; i < m_lits.size(); ++i) {
-            literal l = m_lits[i];
-            out << " " << l << ":"; th.get_context().display_detailed_literal(out, l);            
+        for (literal l : m_lits) {
+            out << l << ":"; th.get_context().display_detailed_literal(out, l) << "\n";           
         }
     }
 
@@ -882,13 +881,10 @@ namespace smt {
         }
         TRACE("derived_bound", 
               tout << "explanation:\n";
-              literal_vector::const_iterator it1  = new_bound->m_lits.begin();
-              literal_vector::const_iterator end1 = new_bound->m_lits.end();
-              for (; it1 != end1; ++it1) tout << *it1 << " ";
+              for (literal l : new_bound->m_lits) tout << l << " ";
               tout << " ";
-              eq_vector::const_iterator it2  = new_bound->m_eqs.begin();
-              eq_vector::const_iterator end2 = new_bound->m_eqs.end();
-              for (; it2 != end2; ++it2) tout << "#" << it2->first->get_owner_id() << "=#" << it2->second->get_owner_id() << " ";
+              for (auto const& e : new_bound->m_eqs) 
+                  tout << "#" << e.first->get_owner_id() << "=#" << e.second->get_owner_id() << " ";
               tout << "\n";);
         DEBUG_CODE(CTRACE("derived_bound", k != val, tout << "k: " << k << ", k_norm: " << k_norm << ", val: " << val << "\n";););
         SASSERT(k == val);
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index cbd41f08c..54f61a09a 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1708,7 +1708,7 @@ namespace smt {
 
     template<typename Ext>
     theory* theory_arith<Ext>::mk_fresh(context* new_ctx) {
-        return alloc(theory_arith<Ext>, new_ctx->get_manager(), m_params);
+        return alloc(theory_arith<Ext>, new_ctx->get_manager(), new_ctx->get_fparams());
     }
 
     template<typename Ext>
@@ -1853,10 +1853,7 @@ namespace smt {
     void theory_arith<Ext>::restore_assignment() {
         CASSERT("arith", valid_row_assignment());
         TRACE("restore_assignment_bug", tout << "START restore_assignment...\n";);
-        typename svector<unsigned>::iterator it  = m_update_trail_stack.begin();
-        typename svector<unsigned>::iterator end = m_update_trail_stack.end();
-        for(; it != end; ++it) {
-            theory_var v = *it;
+        for (theory_var v : m_update_trail_stack) {
             TRACE("restore_assignment_bug", tout << "restoring v" << v << " <- " << m_old_value[v] << "\n";);
             SASSERT(!is_quasi_base(v));
             SASSERT(m_in_update_trail_stack.contains(v));
@@ -2237,11 +2234,7 @@ namespace smt {
         theory_var  best = null_theory_var;
         inf_numeral best_error;
         inf_numeral curr_error;
-        typename var_heap::iterator it  = m_to_patch.begin();
-        typename var_heap::iterator end = m_to_patch.end();
-        //unsigned n = 0;
-        for (; it != end; ++it) {
-            theory_var v = *it;
+        for (theory_var v : m_to_patch) {
             if (below_lower(v))
                 curr_error = lower(v)->get_value() - get_value(v);
             else if (above_upper(v))
@@ -2391,10 +2384,11 @@ namespace smt {
 
         TRACE("sign_row_conflict", tout << "v" << x_i << " is_below: " << is_below << " delta: " << delta << "\n"; display_var(tout, x_i);
               tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";
+              display_row(tout, r, true);
+              display_row(tout, r, false);
               ante.display(tout););
 
         set_conflict(ante, ante, "farkas");
-        // display_bounds_in_smtlib();
     }
 
     // -----------------------------------
@@ -2535,10 +2529,9 @@ namespace smt {
         antecedents ante(*this);
         b1->push_justification(ante, numeral(1), coeffs_enabled());
         b2->push_justification(ante, numeral(1), coeffs_enabled());
-
-        set_conflict(ante, ante, "farkas");
         TRACE("arith_conflict", tout << "bound conflict v" << b1->get_var() << "\n";
               tout << "bounds: " << b1 << " " << b2 << "\n";);
+        set_conflict(ante, ante, "farkas");
     }
 
     // -----------------------------------
@@ -2771,8 +2764,10 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::explain_bound(row const & r, int idx, bool is_lower, inf_numeral & delta, antecedents& ante) {
         SASSERT(delta >= inf_numeral::zero());
-        if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty()))
+        TRACE("arith_conflict", tout << "relax: " << relax_bounds() << " lits: " << ante.lits().size() << " eqs: " << ante.eqs().size() << " idx: " << idx << "\n";);
+        if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty())) {
             return;
+        }
         context & ctx = get_context();
         row_entry const & entry = r[idx];
         numeral           coeff = entry.m_coeff;
@@ -2790,9 +2785,11 @@ namespace smt {
             if (!it->is_dead() && idx != idx2) {
                 bound * b  = get_bound(it->m_var, is_lower ? it->m_coeff.is_pos() : it->m_coeff.is_neg());
                 SASSERT(b);
-                if (!b->has_justification())
+                if (!b->has_justification()) {
                     continue;
+                }
                 if (!relax_bounds() || delta.is_zero()) {
+                    TRACE("propagate_bounds", tout << "push justification: v" << it->m_var << "\n";);
                     b->push_justification(ante, it->m_coeff, coeffs_enabled());
                     continue;
                 }
@@ -2821,10 +2818,7 @@ namespace smt {
                 inf_numeral k_2 = k_1;
                 atom * new_atom = nullptr;
                 atoms const & as           = m_var_occs[it->m_var];
-                typename atoms::const_iterator it  = as.begin();
-                typename atoms::const_iterator end = as.end();
-                for (; it != end; ++it) {
-                    atom * a    = *it;
+                for (atom * a : as) {
                     if (a == b)
                         continue;
                     bool_var bv = a->get_bool_var();
@@ -2880,10 +2874,7 @@ namespace smt {
         atoms const & as                 = m_var_occs[v];
         inf_numeral const & epsilon      = get_epsilon(v);
         inf_numeral delta;
-        typename atoms::const_iterator     it  = as.begin();
-        typename atoms::const_iterator     end = as.end();
-        for (; it != end; ++it) {
-            atom * a = *it;
+        for (atom* a : as) {
             bool_var bv = a->get_bool_var();
             literal  l(bv);
             if (get_context().get_assignment(bv) == l_undef) {
@@ -2954,6 +2945,7 @@ namespace smt {
             TRACE("arith", ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";);
             ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
                                              ante.eqs().size(), ante.eqs().c_ptr(), l);
+
         }
     }
 
@@ -2972,12 +2964,13 @@ namespace smt {
         context & ctx = get_context();
         antecedents ante(*this);
         explain_bound(r, idx, is_lower, delta, ante);
-        dump_lemmas(l, ante);
 
         TRACE("propagate_bounds",
               ante.display(tout) << " --> ";
               ctx.display_detailed_literal(tout, l);
               tout << "\n";);
+        dump_lemmas(l, ante);
+
         if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) {
             literal_vector & lits = m_tmp_literal_vector2;
             lits.reset();
@@ -3060,14 +3053,14 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::set_conflict(antecedents const& ante, antecedents& bounds, char const* proof_rule) {
-        dump_lemmas(false_literal, ante);
         set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule);
+        dump_lemmas(false_literal, ante);
     }
 
     template<typename Ext>
     void theory_arith<Ext>::set_conflict(derived_bound const& ante, antecedents& bounds, char const* proof_rule) {
-        dump_lemmas(false_literal, ante);
         set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule);
+        dump_lemmas(false_literal, ante);
     }
 
     template<typename Ext>
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index ba6648dac..c27d3b44a 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -58,7 +58,6 @@ namespace smt {
     void theory_arith<Ext>::mark_var(theory_var v, svector<theory_var> & vars, var_set & already_found) {
         if (already_found.contains(v))
             return;
-        TRACE("non_linear", tout << "marking: v" << v << "\n";);
         already_found.insert(v);
         vars.push_back(v);
     }
@@ -71,8 +70,7 @@ namespace smt {
         if (is_pure_monomial(v)) {
             expr * n     = var2expr(v);
             SASSERT(m_util.is_mul(n));
-            for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
-                expr * curr  = to_app(n)->get_arg(i);
+            for (expr * curr : *to_app(n)) {
                 theory_var v = expr2var(curr);
                 SASSERT(v != null_theory_var);
                 mark_var(v, vars, already_found);
@@ -118,22 +116,19 @@ namespace smt {
         var_set already_found;
         row_set already_visited_rows;
         context & ctx = get_context();
-        svector<theory_var>::const_iterator it  = m_nl_monomials.begin();
-        svector<theory_var>::const_iterator end = m_nl_monomials.end();
-        for (; it != end; ++it) {
-            theory_var v = *it;
+        for (theory_var v : m_nl_monomials) {
             expr * n     = var2expr(v);
             if (ctx.is_relevant(n))
                 mark_var(v, vars, already_found);
         }
-        for (unsigned idx = 0; idx < vars.size(); idx++) {
-            TRACE("non_linear", tout << "marking dependents of: v" << vars[idx] << "\n";);
-            mark_dependents(vars[idx], vars, already_found, already_visited_rows);
+        // NB: vars changes inside of loop
+        for (unsigned idx = 0; idx < vars.size(); ++idx) {
+            theory_var v = vars[idx];
+            TRACE("non_linear", tout << "marking dependents of: v" << v << "\n";);
+            mark_dependents(v, vars, already_found, already_visited_rows);
         }
         TRACE("non_linear", tout << "variables in non linear cluster:\n";
-              svector<theory_var>::const_iterator it  = vars.begin();
-              svector<theory_var>::const_iterator end = vars.end();
-              for (; it != end; ++it) tout << "v" << *it << " ";
+              for (theory_var v : vars) tout << "v" << v << " ";
               tout << "\n";);
     }
 
@@ -227,9 +222,8 @@ namespace smt {
         SASSERT(!m_util.is_numeral(m));
         if (m_util.is_mul(m)) {
             unsigned num_vars = 0;
-            expr * var        = nullptr;
-            for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
-                expr * curr = to_app(m)->get_arg(i);
+            expr * var = nullptr;
+            for (expr * curr : *to_app(m)) {
                 if (var != curr) {
                     num_vars++;
                     var = curr;
@@ -254,9 +248,7 @@ namespace smt {
             unsigned curr_idx = 0;
             expr * var        = nullptr;
             unsigned power    = 0;
-            unsigned j;
-            for (j = 0; j < to_app(m)->get_num_args(); j++) {
-                expr * arg = to_app(m)->get_arg(j);
+            for (expr * arg : *to_app(m)) {
                 if (var == nullptr) {
                     var   = arg;
                     power = 1;
@@ -360,6 +352,7 @@ namespace smt {
     template<typename Ext>
     interval theory_arith<Ext>::evaluate_as_interval(expr * n) {
         expr* arg;
+        rational val;
         TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";);
         if (has_var(n)) {
             TRACE("nl_evaluate", tout << "n has a variable associated with it\n";);
@@ -370,8 +363,8 @@ namespace smt {
         else if (m_util.is_add(n)) {
             TRACE("nl_evaluate", tout << "is add\n";);
             interval r(m_dep_manager, rational(0));
-            for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
-                r += evaluate_as_interval(to_app(n)->get_arg(i));
+            for (expr* arg : *to_app(n)) {
+                r += evaluate_as_interval(arg);
             }
             TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
             return r;
@@ -388,31 +381,28 @@ namespace smt {
                 it.expt(power);
                 r               *= it;
             }
-            TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
+            TRACE("nl_evaluate", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
             return r;
         }
         else if (m_util.is_to_real(n, arg)) {
             return evaluate_as_interval(arg);
         }
+        else if (m_util.is_numeral(n, val)) {
+            TRACE("nl_evaluate", tout << "is numeral\n";);
+            return interval(m_dep_manager, val);
+        }
         else {
-            rational val;
-            if (m_util.is_numeral(n, val)) {
-                TRACE("nl_evaluate", tout << "is numeral\n";);
-                return interval(m_dep_manager, val);
-            }
-            else {
-                TRACE("nl_evaluate", tout << "is unknown\n";);
-                return interval(m_dep_manager);
-            }
+            TRACE("nl_evaluate", tout << "is unknown\n";);
+            return interval(m_dep_manager);
         }
     }
 
     template<typename Ext>
-    void theory_arith<Ext>::display_monomial(std::ostream & out, expr * m) const {
+    void theory_arith<Ext>::display_monomial(std::ostream & out, expr * n) const {
         bool first = true;
-        unsigned num_vars = get_num_vars_in_monomial(m);
+        unsigned num_vars = get_num_vars_in_monomial(n);
         for (unsigned i = 0; i < num_vars; i++) {
-            var_power_pair p = get_var_and_degree(m, i);
+            var_power_pair p = get_var_and_degree(n, i);
             SASSERT(p.first != 0);
             if (first) first = false; else out << " * ";
             out << mk_bounded_pp(p.first, get_manager()) << "^" << p.second;
@@ -425,10 +415,8 @@ namespace smt {
         m_dep_manager.linearize(dep, bounds);
         m_tmp_lit_set.reset();
         m_tmp_eq_set.reset();
-        ptr_vector<void>::const_iterator it  = bounds.begin();
-        ptr_vector<void>::const_iterator end = bounds.end();
-        for (; it != end; ++it) {
-            bound * b = static_cast<bound*>(*it);
+        for (void* _b : bounds) {
+            bound * b = static_cast<bound*>(_b);
             accumulate_justification(*b, new_bound, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
         }
     }
@@ -544,21 +532,19 @@ namespace smt {
        the method returns without doing anything.
     */
     template<typename Ext>
-    bool theory_arith<Ext>::propagate_nl_downward(expr * m, unsigned i) {
-        SASSERT(is_pure_monomial(m));
-        SASSERT(i < get_num_vars_in_monomial(m));
-        var_power_pair p = get_var_and_degree(m, i);
+    bool theory_arith<Ext>::propagate_nl_downward(expr * n, unsigned i) {
+        SASSERT(is_pure_monomial(n));
+        SASSERT(i < get_num_vars_in_monomial(n));
+        var_power_pair p = get_var_and_degree(n, i);
         expr * v         = p.first;
         unsigned power   = p.second;
-        TRACE("propagate_nl_downward", tout << "m: " << mk_ismt2_pp(m, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) <<
-              "\npower: " << power << "\n";);
         if (power != 1)
             return false; // TODO: remove, when the n-th root is implemented in interval.
-        unsigned num_vars = get_num_vars_in_monomial(m);
+        unsigned num_vars = get_num_vars_in_monomial(n);
         interval other_bounds(m_dep_manager, rational(1));
         // TODO: the following code can be improved it is quadratic on the degree of the monomial.
         for (unsigned i = 0; i < num_vars; i++) {
-            var_power_pair p = get_var_and_degree(m, i);
+            var_power_pair p = get_var_and_degree(n, i);
             if (p.first == v)
                 continue;
             expr * var       = p.first;
@@ -567,7 +553,13 @@ namespace smt {
         }
         if (other_bounds.contains_zero())
             return false; // interval division requires that divisor doesn't contain 0.
-        interval r = mk_interval_for(m);
+        interval r = mk_interval_for(n);
+        TRACE("nl_arith_bug", tout << "m: " << mk_ismt2_pp(n, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) <<
+              "\npower: " << power << "\n";
+              tout << "num_vars: " << num_vars << "\n";
+              display_interval(tout << "monomial bounds\n", r);
+              display_interval(tout << "other bounds\n", other_bounds);
+              );
         r /= other_bounds;
         return update_bounds_using_interval(v, r);
     }
@@ -907,7 +899,6 @@ namespace smt {
             }
             TRACE("non_linear_bug", tout << "enode: " << get_context().get_enode(rhs) << " enode_id: " << get_context().get_enode(rhs)->get_owner_id() << "\n";);
             theory_var new_v = expr2var(rhs);
-            TRACE("non_linear_bug", ctx.display(tout););
             SASSERT(new_v != null_theory_var);
             new_lower    = alloc(derived_bound, new_v, inf_numeral(0), B_LOWER);
             new_upper    = alloc(derived_bound, new_v, inf_numeral(0), B_UPPER);
@@ -953,19 +944,17 @@ namespace smt {
                 }
                 accumulate_justification(*l, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
 
-                TRACE("non_linear",
-                      for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) {
-                          ctx.display_detailed_literal(tout, new_lower->m_lits[j]);
-                          tout << " ";
+                TRACE("non_linear", 
+                      for (literal l : new_lower->m_lits) {
+                          ctx.display_detailed_literal(tout, l) << " ";
                       }
                       tout << "\n";);
 
                 accumulate_justification(*u, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
 
                 TRACE("non_linear",
-                      for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) {
-                          ctx.display_detailed_literal(tout, new_lower->m_lits[j]);
-                          tout << " ";
+                      for (literal l : new_lower->m_lits) {
+                          ctx.display_detailed_literal(tout, l) << " ";
                       }
                       tout << "\n";);
 
@@ -977,9 +966,8 @@ namespace smt {
         TRACE("non_linear",
               new_lower->display(*this, tout << "lower: "); tout << "\n";
               new_upper->display(*this, tout << "upper: "); tout << "\n";
-              for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) {
-                  ctx.display_detailed_literal(tout, new_upper->m_lits[j]);
-                  tout << " ";
+              for (literal lit : new_upper->m_lits) {
+                  ctx.display_detailed_literal(tout, lit) << " ";
               }
               tout << "\n";);
 
@@ -1123,14 +1111,14 @@ namespace smt {
                     continue;
                 if (is_pure_monomial(v)) {
                     expr * m = var2expr(v);
-                    for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
-                        theory_var curr = expr2var(to_app(m)->get_arg(i));
+                    for (expr* arg : *to_app(m)) {
+                        theory_var curr = expr2var(arg);
                         if (m_tmp_var_set.contains(curr))
                             return true;
                     }
                     SASSERT(m == var2expr(v));
-                    for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
-                        theory_var curr = expr2var(to_app(m)->get_arg(i));
+                    for (expr* arg : *to_app(m)) {
+                        theory_var curr = expr2var(arg);
                         if (!is_fixed(curr))
                             m_tmp_var_set.insert(curr);
                     }
@@ -1936,10 +1924,7 @@ namespace smt {
         derived_bound  b(null_theory_var, inf_numeral(0), B_LOWER);
         dependency2new_bound(d, b);
         set_conflict(b, ante, "arith_nl");
-        TRACE("non_linear",
-              for (unsigned i = 0; i < b.m_lits.size(); ++i) {
-                  tout << b.m_lits[i] << " ";
-              });
+        TRACE("non_linear", for (literal lit : b.m_lits) tout << lit << " "; tout << "\n";); 
     }
 
     /**
@@ -2387,7 +2372,7 @@ namespace smt {
 
         elim_quasi_base_rows();
         move_non_base_vars_to_bounds();
-        TRACE("non_linear", tout << "processing non linear constraints...\n"; get_context().display(tout););
+        TRACE("non_linear_verbose", tout << "processing non linear constraints...\n"; get_context().display(tout););
         if (!make_feasible()) {
             TRACE("non_linear", tout << "failed to move variables to bounds.\n";);
             failed();
diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h
index 6579856a4..59d386292 100644
--- a/src/smt/theory_arith_pp.h
+++ b/src/smt/theory_arith_pp.h
@@ -391,19 +391,19 @@ namespace smt {
     void theory_arith<Ext>::display_vars(std::ostream & out) const {
         out << "vars:\n";
         int n = get_num_vars();
-		int inf_vars = 0;
-		int int_inf_vars = 0;
-		for (theory_var v = 0; v < n; v++) {
-			if ((lower(v) && lower(v)->get_value() > get_value(v))
-				|| (upper(v) && upper(v)->get_value() < get_value(v)))
-				inf_vars++;
-			if (is_int(v) && !get_value(v).is_int())
-				int_inf_vars++;
-		}
-		out << "infeasibles = " << inf_vars << " int_inf = " << int_inf_vars << std::endl;
-		for (theory_var v = 0; v < n; v++) {
-			display_var(out, v);
-		}
+        int inf_vars = 0;
+        int int_inf_vars = 0;
+        for (theory_var v = 0; v < n; v++) {
+            if ((lower(v) && lower(v)->get_value() > get_value(v))
+                || (upper(v) && upper(v)->get_value() < get_value(v)))
+                inf_vars++;
+            if (is_int(v) && !get_value(v).is_int())
+                int_inf_vars++;
+        }
+        out << "infeasibles = " << inf_vars << " int_inf = " << int_inf_vars << std::endl;
+        for (theory_var v = 0; v < n; v++) {
+            display_var(out, v);
+        }
     }
 
     template<typename Ext>
@@ -418,9 +418,9 @@ namespace smt {
         th.get_context().display_literals_verbose(out, lits().size(), lits().c_ptr());
         if (!lits().empty()) out << "\n";
         ast_manager& m = th.get_manager();
-        for (unsigned i = 0; i < m_eqs.size(); ++i) {
-            out << mk_pp(m_eqs[i].first->get_owner(), m) << " ";
-            out << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";            
+        for (auto const& e : m_eqs) {
+            out << mk_pp(e.first->get_owner(), m) << " ";
+            out << mk_pp(e.second->get_owner(), m) << "\n";            
         }
         return out;
     }
@@ -431,27 +431,24 @@ namespace smt {
         m_dep_manager.linearize(dep, bounds);
         m_tmp_lit_set.reset();
         m_tmp_eq_set.reset();
-        ptr_vector<void>::const_iterator it  = bounds.begin();
-        ptr_vector<void>::const_iterator end = bounds.end();
-        for (; it != end; ++it) {
-            bound * b = static_cast<bound*>(*it);
-            out << " ";
-            b->display(*this, out);
+        for (void *_b : bounds) {
+            bound * b = static_cast<bound*>(_b);
+            b->display(*this, out << "\n");
         }
     }
 
     template<typename Ext>
     void theory_arith<Ext>::display_interval(std::ostream & out, interval const& i) {
         i.display(out);
-        display_deps(out << " lo:", i.get_lower_dependencies());
-        display_deps(out << " hi:", i.get_upper_dependencies());
+        display_deps(out << "\nlo:", i.get_lower_dependencies());
+        display_deps(out << "\nhi:", i.get_upper_dependencies());
     }
 
     template<typename Ext>
     void theory_arith<Ext>::display_atoms(std::ostream & out) const {
         out << "atoms:\n";
-        for (unsigned i = 0; i < m_atoms.size(); i++)
-            display_atom(out, m_atoms[i], false);
+        for (atom * a : m_atoms) 
+            display_atom(out, a, false);
     }
 
     template<typename Ext>
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 873d1692d..a0c62b959 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -138,9 +138,9 @@ namespace smt {
 
     void theory_bv::process_args(app * n) {
         context & ctx     = get_context();
-        unsigned num_args = n->get_num_args();
-        for (unsigned i = 0; i < num_args; i++)
-            ctx.internalize(n->get_arg(i), false);
+        for (expr* arg : *n) {
+            ctx.internalize(arg, false);
+        }
     }
 
     enode * theory_bv::mk_enode(app * n) {
@@ -161,6 +161,8 @@ namespace smt {
         theory_var v = n->get_th_var(get_id());
         if (v == null_theory_var) {
             v = mk_var(n);
+        }
+        if (m_bits[v].empty()) {
             mk_bits(v);
         }
         return v;
@@ -185,11 +187,9 @@ namespace smt {
     void theory_bv::get_bits(theory_var v, expr_ref_vector & r) {
         context & ctx         = get_context();
         literal_vector & bits = m_bits[v];
-        literal_vector::const_iterator it  = bits.begin();
-        literal_vector::const_iterator end = bits.end();
-        for (; it != end; ++it) {
+        for (literal lit : bits) {
             expr_ref l(get_manager());
-            ctx.literal2expr(*it, l);
+            ctx.literal2expr(lit, l);
             r.push_back(l);
         }
     }
@@ -358,18 +358,16 @@ namespace smt {
 
         void mark_bits(conflict_resolution & cr, literal_vector const & bits) {
             context & ctx = cr.get_context();
-            literal_vector::const_iterator it  = bits.begin();
-            literal_vector::const_iterator end = bits.end();
-            for (; it != end; ++it) {
-                if (it->var() != true_bool_var) {
-                    if (ctx.get_assignment(*it) == l_true)
-                        cr.mark_literal(*it);
+            for (literal lit : bits) {
+                if (lit.var() != true_bool_var) {
+                    if (ctx.get_assignment(lit) == l_true)
+                        cr.mark_literal(lit);
                     else
-                        cr.mark_literal(~(*it));
+                        cr.mark_literal(~lit);
                 }
             }
         }
-
+        
         void get_proof(conflict_resolution & cr, literal l, ptr_buffer<proof> & prs, bool & visited) {
             if (l.var() == true_bool_var)
                 return;
@@ -830,10 +828,9 @@ namespace smt {
         while (i > 0) {
             i--;
             theory_var arg = get_arg_var(e, i);
-            literal_vector::const_iterator it  = m_bits[arg].begin();
-            literal_vector::const_iterator end = m_bits[arg].end();
-            for (; it != end; ++it)
-                add_bit(v, *it);
+            for (literal lit : m_bits[arg]) {
+                add_bit(v, lit);
+            }
         }
         find_wpos(v);
     }
@@ -1308,10 +1305,9 @@ namespace smt {
             theory_var v = e->get_th_var(get_id());
             if (v != null_theory_var) {
                 literal_vector & bits        = m_bits[v];
-                literal_vector::iterator it  = bits.begin();
-                literal_vector::iterator end = bits.end();
-                for (; it != end; ++it)
-                    ctx.mark_as_relevant(*it);
+                for (literal lit : bits) {
+                    ctx.mark_as_relevant(lit);
+                }
             }
         }
     }
@@ -1463,35 +1459,27 @@ namespace smt {
         SASSERT(bv_size == get_bv_size(r2));
         m_merge_aux[0].reserve(bv_size+1, null_theory_var);
         m_merge_aux[1].reserve(bv_size+1, null_theory_var);
-#define RESET_MERGET_AUX() {                                                    \
-            zero_one_bits::iterator it  = bits1.begin();                        \
-            zero_one_bits::iterator end = bits1.end();                          \
-            for (; it != end; ++it)                                             \
-                m_merge_aux[it->m_is_true][it->m_idx] = null_theory_var;        \
-        }
+
+#define RESET_MERGET_AUX()  for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = null_theory_var; 
+
         DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) { SASSERT(m_merge_aux[0][i] == null_theory_var || m_merge_aux[1][i] == null_theory_var); });
         // save info about bits1
-        zero_one_bits::iterator it  = bits1.begin();
-        zero_one_bits::iterator end = bits1.end();
-        for (; it != end; ++it)
-            m_merge_aux[it->m_is_true][it->m_idx] = it->m_owner;
+        for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = zo.m_owner;
         // check if bits2 is consistent with bits1, and copy new bits to bits1
-        it  = bits2.begin();
-        end = bits2.end();
-        for (; it != end; ++it) {
-            theory_var v2 = it->m_owner;
-            theory_var v1 = m_merge_aux[!it->m_is_true][it->m_idx];
+        for (auto & zo : bits2) {
+            theory_var v2 = zo.m_owner;
+            theory_var v1 = m_merge_aux[!zo.m_is_true][zo.m_idx];
             if (v1 != null_theory_var) {
                 // conflict was detected ... v1 and v2 have complementary bits
-                SASSERT(m_bits[v1][it->m_idx] == ~(m_bits[v2][it->m_idx]));
+                SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx]));
                 SASSERT(m_bits[v1].size() == m_bits[v2].size());
-                mk_new_diseq_axiom(v1, v2, it->m_idx);
+                mk_new_diseq_axiom(v1, v2, zo.m_idx);
                 RESET_MERGET_AUX();
                 return false;
             }
-            if (m_merge_aux[it->m_is_true][it->m_idx] == null_theory_var) {
+            if (m_merge_aux[zo.m_is_true][zo.m_idx] == null_theory_var) {
                 // copy missing variable to bits1
-                bits1.push_back(*it);
+                bits1.push_back(zo);
             }
         }
         // reset m_merge_aux vector
@@ -1614,11 +1602,9 @@ namespace smt {
         out << std::right << ", bits:";
         context & ctx = get_context();
         literal_vector const & bits = m_bits[v];
-        literal_vector::const_iterator it  = bits.begin();
-        literal_vector::const_iterator end = bits.end();
-        for (; it != end; ++it) {
+        for (literal lit : bits) {
             out << " ";
-            ctx.display_literal(out, *it);
+            ctx.display_literal(out, lit);
         }
         numeral val;
         if (get_fixed_value(v, val))
@@ -1740,13 +1726,11 @@ namespace smt {
             SASSERT(_bits.size() == num_bits);
             svector<bool> already_found;
             already_found.resize(bv_sz, false);
-            zero_one_bits::const_iterator it  = _bits.begin();
-            zero_one_bits::const_iterator end = _bits.end();
-            for (; it != end; ++it) {
-                SASSERT(find(it->m_owner) == v);
-                SASSERT(bits[it->m_is_true][it->m_idx]);
-                SASSERT(!already_found[it->m_idx]);
-                already_found[it->m_idx] = true;
+            for (auto & zo : _bits) {
+                SASSERT(find(zo.m_owner) == v);
+                SASSERT(bits[zo.m_is_true][zo.m_idx]);
+                SASSERT(!already_found[zo.m_idx]);
+                already_found[zo.m_idx] = true;
             }
         }
         return true;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index a057ace03..a49e0e4bb 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -516,7 +516,7 @@ class theory_lra::imp {
         rational r1;
         v = mk_var(t);
         svector<lp::var_index> vars;
-        ptr_vector<expr> todo;
+        ptr_buffer<expr> todo;
         todo.push_back(t);
         while (!todo.empty()) {
             expr* n = todo.back();
@@ -536,7 +536,7 @@ class theory_lra::imp {
                 vars.push_back(get_var_index(mk_var(n)));
             }
         }
-        TRACE("arith", tout << mk_pp(t, m) << " " << _has_var << "\n";);
+        TRACE("arith", tout << "v" << v << "(" << get_var_index(v) << ") := " << mk_pp(t, m) << " " << _has_var << "\n";);
         if (!_has_var) {
             ensure_nra();
             m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
@@ -1190,12 +1190,12 @@ public:
             if (m_solver->is_term(wi)) {
                 const lp::lar_term& term = m_solver->get_term(wi);
                 result += term.m_v * coeff;
-                for (const auto & i : term.m_coeffs) {
-                    if (m_variable_values.count(i.first) > 0) {
-                        result += m_variable_values[i.first] * coeff * i.second;
+                for (const auto & i : term) {
+                    if (m_variable_values.count(i.var()) > 0) {
+                        result += m_variable_values[i.var()] * coeff * i.coeff();
                     }
                     else {
-                        m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second));
+                        m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
                     }
                 }                    
             }
@@ -1481,7 +1481,7 @@ public:
         }
         if (!m_nra) return l_true;
         if (!m_nra->need_check()) return l_true;
-        m_a1 = 0; m_a2 = 0;
+        m_a1 = nullptr; m_a2 = nullptr;
         lbool r = m_nra->check(m_explanation);
         m_a1 = alloc(scoped_anum, m_nra->am());
         m_a2 = alloc(scoped_anum, m_nra->am());
@@ -2153,8 +2153,8 @@ public:
             vi = m_todo_vars.back();
             m_todo_vars.pop_back();
             lp::lar_term const& term = m_solver->get_term(vi);
-            for (auto const& coeff : term.m_coeffs) {
-                lp::var_index wi = coeff.first;
+            for (auto const& coeff : term) {
+                lp::var_index wi = coeff.var();
                 if (m_solver->is_term(wi)) {
                     m_todo_vars.push_back(wi);
                 }
@@ -2605,19 +2605,23 @@ public:
 
             m_todo_terms.push_back(std::make_pair(vi, rational::one()));
 
+            TRACE("arith", tout << "v" << v << " := w" << vi << "\n";
+                  m_solver->print_term(m_solver->get_term(vi), tout); tout << "\n";);
+
             m_nra->am().set(r, 0);
             while (!m_todo_terms.empty()) {
                 rational wcoeff = m_todo_terms.back().second;
-                //                 lp::var_index wi = m_todo_terms.back().first; // todo : got a warning "wi is not used"
+                vi = m_todo_terms.back().first;
                 m_todo_terms.pop_back();
                 lp::lar_term const& term = m_solver->get_term(vi);
+                TRACE("arith", m_solver->print_term(term, tout); tout << "\n";);
                 scoped_anum r1(m_nra->am());
                 rational c1 = term.m_v * wcoeff;
                 m_nra->am().set(r1, c1.to_mpq());
                 m_nra->am().add(r, r1, r);                
-                for (auto const coeff : term.m_coeffs) {
-                    lp::var_index wi = coeff.first;
-                    c1 = coeff.second * wcoeff;
+                for (auto const & arg : term) {
+                    lp::var_index wi = m_solver->local2external(arg.var());
+                    c1 = arg.coeff() * wcoeff;
                     if (m_solver->is_term(wi)) {
                         m_todo_terms.push_back(std::make_pair(wi, c1));
                     }
@@ -2648,6 +2652,7 @@ public:
         else {
             rational r = get_value(v);
             TRACE("arith", tout << "v" << v << " := " << r << "\n";);
+            SASSERT(!a.is_int(o) || r.is_int());
             if (a.is_int(o) && !r.is_int()) r = floor(r);
             return alloc(expr_wrapper_proc, m_factory->mk_value(r,  m.get_sort(o)));
         }
@@ -2797,6 +2802,7 @@ public:
             lp::var_index vi = m_theory_var2var_index[v];
             st = m_solver->maximize_term(vi, term_max);
         }
+        TRACE("arith", display(tout << st << " v" << v << "\n"););
         switch (st) {
         case lp::lp_status::OPTIMAL: {
             inf_rational val(term_max.x, term_max.y);
@@ -2804,13 +2810,12 @@ public:
             return inf_eps(rational::zero(), val);
         }
         case lp::lp_status::FEASIBLE: {
-            inf_rational val(term_max.x, term_max.y);
+            inf_rational val = get_value(v);
             blocker = mk_gt(v);
             return inf_eps(rational::zero(), val);
         }
         default:
             SASSERT(st == lp::lp_status::UNBOUNDED);
-            TRACE("arith", tout << "Unbounded v" << v << "\n";);
             has_shared = false;
             blocker = m.mk_false();
             return inf_eps(rational::one(), inf_rational());
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 48d4ddcc0..8f64544b4 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -889,38 +889,35 @@ bool theory_seq::branch_quat_variable(eq const& e) {
     return true;
 }
 
-void theory_seq::len_offset(expr* const& e, rational val) {
+void theory_seq::len_offset(expr* e, rational val) {
     context & ctx = get_context();
     expr *l1 = nullptr, *l2 = nullptr, *l21 = nullptr, *l22 = nullptr;
     rational fact;
     if (m_autil.is_add(e, l1, l2) && m_autil.is_mul(l2, l21, l22) &&
-            m_autil.is_numeral(l21, fact) && fact.is_minus_one()) {
+        m_autil.is_numeral(l21, fact) && fact.is_minus_one()) {
         if (ctx.e_internalized(l1) && ctx.e_internalized(l22)) {
             enode* r1 = ctx.get_enode(l1)->get_root(), *n1 = r1;
             enode* r2 = ctx.get_enode(l22)->get_root(), *n2 = r2;
             expr *e1 = nullptr, *e2 = nullptr;
             do {
-                if (!m_util.str.is_length(n1->get_owner(), e1))
-                    n1 = n1->get_next();
-                else
+                if (m_util.str.is_length(n1->get_owner(), e1))
                     break;
+                n1 = n1->get_next();               
             }
             while (n1 != r1);
             do {
-                if (!m_util.str.is_length(n2->get_owner(), e2))
-                    n2 = n2->get_next();
-                else
+                if (m_util.str.is_length(n2->get_owner(), e2)) 
                     break;
+                n2 = n2->get_next();                
             }
             while (n2 != r2);
+            obj_map<enode, int> tmp;
             if (m_util.str.is_length(n1->get_owner(), e1)
-            && m_util.str.is_length(n2->get_owner(), e2)) {
-                obj_map<enode, int> tmp;
-                m_len_offset.find(r1, tmp);
+                && m_util.str.is_length(n2->get_owner(), e2) &&                
+                m_len_offset.find(r1, tmp)) {
                 tmp.insert(r2, val.get_int32());
                 m_len_offset.insert(r1, tmp);
-                TRACE("seq", tout << "a length pair: " << mk_pp(e1, m)
-                << ", " << mk_pp(e2, m) << "\n";);
+                TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) << ", " << mk_pp(e2, m) << "\n";);
                 return;
             }
         }
@@ -1307,32 +1304,34 @@ bool theory_seq::len_based_split(eq const& e) {
             y12 = mk_concat(Z, y12);
         }
     }
-    else
-        lenY11 = m_util.str.mk_length(y11);
+	else {
+		lenY11 = m_util.str.mk_length(y11);
+	}
 
     dependency* dep = e.dep();
     literal_vector lits;
     literal lit1 = mk_eq(lenX11, lenY11, false);
+	if (ctx.get_assignment(lit1) != l_true) {
+		return false;
+	}
     lits.push_back(lit1);
 
-    if (ls.size()>=2 && rs.size()>=2 && (ls.size()>2 || rs.size()>2)) {
+    if (ls.size() >= 2 && rs.size() >= 2 && (ls.size() > 2 || rs.size() > 2)) {
         expr_ref len1(m_autil.mk_int(0),m), len2(m_autil.mk_int(0),m);
         for (unsigned i = 2; i < ls.size(); ++i)
             len1 = mk_add(len1, m_util.str.mk_length(ls[i]));
         for (unsigned i = 2; i < rs.size(); ++i)
             len2 = mk_add(len2, m_util.str.mk_length(rs[i]));
-        bool flag = false;
+		literal lit2;
         if (!m_autil.is_numeral(len1) && !m_autil.is_numeral(len2)) {
-            literal lit2 = mk_eq(len1, len2, false);
-            flag = ctx.get_assignment(lit2) == l_true;
+            lit2 = mk_eq(len1, len2, false);           
         }
         else {
             expr_ref eq_len(m.mk_eq(len1, len2), m);
-            flag = ctx.find_assignment(eq_len) == l_true;
+			lit2 = mk_literal(eq_len);            
         }
         
-        if (flag) {
-            literal lit2 = mk_eq(len1, len2, false);
+        if (ctx.get_assignment(lit2) == l_true) {           
             lits.push_back(lit2);
             TRACE("seq", tout << mk_pp(len1, m) << " = " << mk_pp(len2, m) << "\n";);
             expr_ref lhs(m), rhs(m);
@@ -4582,7 +4581,6 @@ bool theory_seq::lower_bound(expr* _e, rational& lo) const {
         if (thi && thi->get_lower(ctx.get_enode(e), _lo)) break;
         theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
         if (thr && thr->get_lower(ctx.get_enode(e), _lo)) break;
-        TRACE("seq", tout << "no lower bound " << mk_pp(_e, m) << "\n";);
         return false;
     }
     while (false);
@@ -4640,7 +4638,6 @@ bool theory_seq::upper_bound(expr* _e, rational& hi) const {
         if (thi && thi->get_upper(ctx.get_enode(e), _hi)) break;
         theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
         if (thr && thr->get_upper(ctx.get_enode(e), _hi)) break;
-        TRACE("seq", tout << "no upper bound " << mk_pp(_e, m) << "\n";);
         return false;
     }
     while (false);
@@ -5163,7 +5160,22 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
         }
     }
     else if (m_util.str.is_contains(e, e1, e2)) {
-        if (is_true) {
+        expr_ref_vector disj(m);
+        // disabled pending regression on issue 1196
+        if (false && m_seq_rewrite.reduce_contains(e1, e2, disj)) {
+            literal_vector lits;
+            literal lit = mk_literal(e);
+            lits.push_back(~lit);
+            for (expr* d : disj) {
+                lits.push_back(mk_literal(d));
+            }
+            ++m_stats.m_add_axiom;            
+            ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+            for (expr* d : disj) {
+                add_axiom(lit, ~mk_literal(d));
+            }
+        }
+        else if (is_true) {
             expr_ref f1 = mk_skolem(m_indexof_left, e1, e2);
             expr_ref f2 = mk_skolem(m_indexof_right, e1, e2);
             f = mk_concat(f1, e2, f2);
@@ -5263,9 +5275,10 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
 
 void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
     enode* n1 = get_enode(v1);
-    enode* n2 = get_enode(v2);
+    enode* n2 = get_enode(v2);    
     expr_ref e1(n1->get_owner(), m);
     expr_ref e2(n2->get_owner(), m);
+    SASSERT(n1->get_root() != n2->get_root());
     m_exclude.update(e1, e2);
     expr_ref eq(m.mk_eq(e1, e2), m);
     TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index abb202884..23b044445 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -375,7 +375,7 @@ namespace smt {
 
         void init_model(expr_ref_vector const& es);
         
-        void len_offset(expr* const& e, rational val);
+        void len_offset(expr* e, rational val);
         void prop_arith_to_len_offset();
         int find_fst_non_empty_idx(expr_ref_vector const& x) const;
         expr* find_fst_non_empty_var(expr_ref_vector const& x) const;
diff --git a/src/util/approx_nat.h b/src/util/approx_nat.h
index b5e1edb8f..354ead92b 100644
--- a/src/util/approx_nat.h
+++ b/src/util/approx_nat.h
@@ -21,7 +21,7 @@ Notes:
 #define APPROX_NAT_H_
 
 #include<iostream>
-#include<limits.h>
+#include<climits>
 
 class approx_nat {
     unsigned m_value;
diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp
index f9f0a0797..78b7f15aa 100644
--- a/src/util/bit_vector.cpp
+++ b/src/util/bit_vector.cpp
@@ -16,7 +16,7 @@ Author:
 Revision History:
 
 --*/
-#include<limits.h>
+#include<climits>
 #include "util/bit_vector.h"
 #include "util/trace.h"
 
diff --git a/src/util/fixed_bit_vector.cpp b/src/util/fixed_bit_vector.cpp
index aafc58404..e227aa524 100644
--- a/src/util/fixed_bit_vector.cpp
+++ b/src/util/fixed_bit_vector.cpp
@@ -19,7 +19,7 @@ Revision History:
 
 --*/
 
-#include<limits.h>
+#include<climits>
 #include "util/fixed_bit_vector.h"
 #include "util/trace.h"
 #include "util/hash.h"
diff --git a/src/util/hashtable.h b/src/util/hashtable.h
index 420e48949..55866065e 100644
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@@ -19,9 +19,9 @@ Revision History:
 #ifndef HASHTABLE_H_
 #define HASHTABLE_H_
 #include "util/debug.h"
-#include<ostream>
+#include <ostream>
 #include "util/util.h"
-#include<limits.h>
+#include <climits>
 #include "util/memory_manager.h"
 #include "util/hash.h"
 #include "util/vector.h"
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 0cfdc33b4..c4f7ff196 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -538,8 +538,11 @@ lp_status lar_solver::maximize_term(unsigned ext_j,
         if (column_value_is_integer(j))
             continue;
         if (m_int_solver->is_base(j)) {
-            if (!remove_from_basis(j)) // consider a special version of remove_from_basis that would not remove inf_int columns
+            if (!remove_from_basis(j)) { // consider a special version of remove_from_basis that would not remove inf_int columns
+                m_mpq_lar_core_solver.m_r_x = backup;
+                term_max = prev_value;
                 return lp_status::FEASIBLE; // it should not happen
+            }
         }
         m_int_solver->patch_nbasic_column(j, false);
         if (!column_value_is_integer(j)) {
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 3735fbb9f..283c13c38 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -247,6 +247,8 @@ public:
     void calculate_implied_bounds_for_row(unsigned i, bound_propagator & bp);
 
     unsigned adjust_column_index_to_term_index(unsigned j) const;
+
+    var_index local2external(var_index idx) const { return m_var_register.local_to_external(idx); }
     
     void propagate_bounds_on_a_term(const lar_term& t, bound_propagator & bp, unsigned term_offset);
 
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
index a4930b357..0d28058e8 100644
--- a/src/util/lp/nra_solver.cpp
+++ b/src/util/lp/nra_solver.cpp
@@ -24,11 +24,12 @@ namespace nra {
         lp::lar_solver&      s;
         reslimit&              m_limit;  
         params_ref             m_params; 
-        u_map<polynomial::var> m_lp2nl;  // map from lar_solver variables to nlsat::solver variables
+        u_map<polynomial::var> m_lp2nl;  // map from lar_solver variables to nlsat::solver variables        
         scoped_ptr<nlsat::solver>  m_nlsat;
+        scoped_ptr<scoped_anum>    m_zero;
         vector<mon_eq>         m_monomials;
         unsigned_vector        m_monomials_lim;
-        mutable std::unordered_map<lp::var_index, rational> m_variable_values; // current model
+        mutable std::unordered_map<lp::var_index, rational> m_variable_values; // current model        
 
         imp(lp::lar_solver& s, reslimit& lim, params_ref const& p): 
             s(s), 
@@ -90,6 +91,7 @@ namespace nra {
         lbool check(lp::explanation_t& ex) {
             SASSERT(need_check());
             m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
+            m_zero = alloc(scoped_anum, am());
             m_lp2nl.reset();
             vector<nlsat::assumption, false> core;
 
@@ -208,12 +210,17 @@ namespace nra {
             if (!m_lp2nl.find(v, r)) {
                 r = m_nlsat->mk_var(is_int(v));
                 m_lp2nl.insert(v, r);
+                TRACE("arith", tout << "v" << v << " := x" << r << "\n";);
             }
             return r;
         }
 
         nlsat::anum const& value(lp::var_index v) const {
-           return m_nlsat->value(m_lp2nl.find(v));
+            polynomial::var pv;
+            if (m_lp2nl.find(v, pv))
+                return m_nlsat->value(pv);
+            else
+                return *m_zero;
         }
 
         nlsat::anum_manager& am() {
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 59a6cb009..0a1d360c8 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -6,7 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 #include<iostream>
 #include<stdlib.h>
-#include<limits.h>
+#include<climits>
 #include "util/trace.h"
 #include "util/memory_manager.h"
 #include "util/error_codes.h"
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 187532a87..65f89f078 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -19,7 +19,6 @@ Revision History:
 #ifndef MPZ_H_
 #define MPZ_H_
 
-#include<limits.h>
 #include<string>
 #include "util/util.h"
 #include "util/small_object_allocator.h"
diff --git a/src/util/nat_set.h b/src/util/nat_set.h
index 6e9ab1b6d..f2f2cb8e1 100644
--- a/src/util/nat_set.h
+++ b/src/util/nat_set.h
@@ -19,7 +19,7 @@ Revision History:
 #ifndef NAT_SET_H_
 #define NAT_SET_H_
 
-#include<limits.h>
+#include <climits>
 #include "util/vector.h"
 
 class nat_set {
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index 56d40c47a..8078c46ee 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -50,7 +50,7 @@ Revision History:
 #undef max
 #endif
 #include "util/util.h"
-#include<limits.h>
+#include<climits>
 #include "util/z3_omp.h"
 
 struct scoped_timer::imp {
diff --git a/src/util/symbol.h b/src/util/symbol.h
index 88e825551..40844cf3b 100644
--- a/src/util/symbol.h
+++ b/src/util/symbol.h
@@ -19,7 +19,7 @@ Revision History:
 #ifndef SYMBOL_H_
 #define SYMBOL_H_
 #include<ostream>
-#include<limits.h>
+#include<climits>
 
 #include "util/util.h"
 #include "util/tptr.h"