diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 7b508c7d8..2e65fddc9 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4373,7 +4373,7 @@ namespace smt {
     void context::add_rec_funs_to_model() {
         ast_manager& m = m_manager;
         SASSERT(m_model);
-        for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) {
+        for (unsigned i = 0; !get_cancel_flag() && i < m_asserted_formulas.get_num_formulas(); ++i) {
             expr* e = m_asserted_formulas.get_formula(i);
             if (is_quantifier(e)) {
                 TRACE("context", tout << mk_pp(e, m) << "\n";);
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 3cc577b29..c6cca2c43 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -209,7 +209,12 @@ namespace smt {
             ~scoped_mk_model() {
                 if (m_ctx.m_proto_model.get() != 0) {
                     m_ctx.m_model = m_ctx.m_proto_model->mk_model();
-                    m_ctx.add_rec_funs_to_model();
+                    try {
+                        m_ctx.add_rec_funs_to_model();
+                    }
+                    catch (...) {
+                        // no op
+                    }
                     m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
                 }
             }
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index a1f0f9777..17f889946 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -47,6 +47,8 @@ namespace smt {
         sLevel(0),
         finalCheckProgressIndicator(false),
         m_trail(m),
+        m_factory(nullptr),
+        m_unused_id(0),
         m_delayed_axiom_setup_terms(m),
         tmpStringVarCount(0),
         tmpXorVarCount(0),
@@ -4648,14 +4650,17 @@ namespace smt {
     // We only check m_find for a string constant.
 
     expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) {
-        expr * curr = n;
+        theory_var curr = m_find.find(get_var(n));
+        theory_var first = curr;
         do {
-            if (u.str.is_string(curr)) {
+            expr* a = get_ast(curr);
+            if (u.str.is_string(a)) {
                 hasEqcValue = true;
-                return curr;
+                return a;
             }
-            curr = get_eqc_next(curr);
-        } while (curr != n);
+            curr = m_find.next(curr);
+        } 
+        while (curr != first && curr != null_theory_var);
         hasEqcValue = false;
         return n;
     }
@@ -10584,7 +10589,9 @@ namespace smt {
             return alloc(expr_wrapper_proc, val);
         } else {
             TRACE("str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;);
-            return alloc(expr_wrapper_proc, to_app(mk_string("**UNUSED**")));
+            std::ostringstream unused;
+            unused << "**UNUSED**" << (m_unused_id++);
+            return alloc(expr_wrapper_proc, to_app(mk_string(unused.str().c_str())));
         }
     }
 
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index acac8cad1..b478808d2 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -267,6 +267,10 @@ protected:
 
     str_value_factory * m_factory;
 
+    // Unique identifier appended to unused variables to ensure that model construction
+    // does not introduce equalities when they weren't enforced.
+    unsigned m_unused_id;
+
     // terms we couldn't go through set_up_axioms() with because they weren't internalized
     expr_ref_vector m_delayed_axiom_setup_terms;