diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 52b87e536..513c68d6e 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -84,6 +84,9 @@ namespace opt {
                 if (m.canceled()) {
                     is_sat = l_undef;
                 }
+                if (is_sat == l_undef) {
+                    break;
+                }
                 if (is_sat == l_false) {
                     TRACE("opt", tout << "Unsat\n";);
                     break;
@@ -97,9 +100,6 @@ namespace opt {
                     //DEBUG_CODE(verify_cores(cores););
                     s().assert_expr(fml);
                 }
-                else {
-                    //DEBUG_CODE(verify_cores(cores););
-                }
                 update_cores(wth(), cores);
                 wth().init_min_cost(m_upper - m_lower);
                 trace_bounds("wmax");
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 0f9d42b3d..126594b06 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8096,7 +8096,7 @@ namespace smt {
             rational nn1Len, nn2Len;
             bool nn1Len_exists = get_len_value(lhs, nn1Len);
             bool nn2Len_exists = get_len_value(rhs, nn2Len);
-            expr * emptyStr = mk_string("");
+            expr_ref emptyStr(mk_string(""), m);
 
             if (nn1Len_exists && nn1Len.is_zero()) {
                 if (!in_same_eqc(lhs, emptyStr) && rhs != emptyStr) {