diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp
index 43e7bdff8..773f328ab 100644
--- a/src/interp/iz3base.cpp
+++ b/src/interp/iz3base.cpp
@@ -281,7 +281,7 @@ bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof, std::vector<ast> &v
         _proof = cook(proof);
     }
     else if(vars.size()) {
-        model_ref(_m);
+        model_ref _m;
         s.get_model(_m);
         if (!_m.get()) {
             SASSERT(l_undef == res);
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 0c4d11420..dde75c4bc 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -6768,7 +6768,7 @@ namespace smt {
         expr * sub2;
         if (u.re.is_to_re(re, sub1)) {
             SASSERT(u.str.is_string(sub1));
-            zstring(str);
+            zstring str;
             u.str.is_string(sub1, str);
             lens.insert(str.length());
         } else if (u.re.is_concat(re, sub1, sub2)) {