diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 4102f5d80..97f0d6369 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1000,12 +1000,12 @@ namespace smt {
      * Length(Concat(x, y)) = Length(x) + Length(y)
      */
     void theory_str::instantiate_concat_axiom(enode * cat) {
-        app * a_cat = cat->get_owner();
-        SASSERT(u.str.is_concat(a_cat));
-
         ast_manager & m = get_manager();
-
+        app * a_cat = cat->get_owner();
         TRACE("str", tout << "instantiating concat axiom for " << mk_ismt2_pp(a_cat, m) << std::endl;);
+        if (!u.str.is_concat(a_cat)) {
+            return;
+        }
 
         // build LHS
         expr_ref len_xy(m);
@@ -7214,6 +7214,13 @@ namespace smt {
         TRACE("str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;);
         candidate_model.reset();
 
+        m_basicstr_axiom_todo.reset();
+        m_concat_axiom_todo.reset();
+        m_concat_eval_todo.reset();
+        m_library_aware_axiom_todo.reset();
+        m_delayed_axiom_setup_terms.reset();
+        m_delayed_assertions_todo.reset();
+        
         TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); });
 
         // list of expr* to remove from cut_var_map
diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index 9da3f3876..b6520d80e 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -686,8 +686,14 @@ namespace smt {
             rational pos, len;
             bool pos_exists = v.get_value(arg1, pos);
             bool len_exists = v.get_value(arg2, len);
-            ENSURE(pos_exists);
-            ENSURE(len_exists);
+            if (!pos_exists) {
+                cex = expr_ref(m.mk_or(m_autil.mk_ge(arg1, mk_int(0)), m_autil.mk_le(arg1, mk_int(0))), m);
+                return false;
+            }
+            if (!len_exists) {
+                cex = expr_ref(m.mk_or(m_autil.mk_ge(arg2, mk_int(0)), m_autil.mk_le(arg2, mk_int(0))), m);
+                return false;
+            }
             TRACE("str_fl", tout << "reduce substring term: base=" << mk_pp(term, m) << " (length="<<base_chars.size()<<"), pos=" << pos.to_string() << ", len=" << len.to_string() << std::endl;);
             // Case 1: pos < 0 or pos >= strlen(base) or len < 0
             // ==> (Substr ...) = ""