diff --git a/src/muz/pdr/pdr_sym_mux.h b/src/muz/pdr/pdr_sym_mux.h
index bc1819539..78025f26b 100644
--- a/src/muz/pdr/pdr_sym_mux.h
+++ b/src/muz/pdr/pdr_sym_mux.h
@@ -23,6 +23,7 @@ Revision History:
 #include "ast.h"
 #include "map.h"
 #include "vector.h"
+#include <vector>
 
 class model_core;
 
@@ -46,7 +47,7 @@ private:
     mutable unsigned       m_next_sym_suffix_idx;
     mutable symbols        m_used_suffixes;
     /** Here we have default suffixes for each of the variants */
-    vector<std::string>    m_suffixes;
+    std::vector<std::string>    m_suffixes;
 
 
     /**
diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp
index 6e3a1f441..0b509fba6 100644
--- a/src/test/model_evaluator.cpp
+++ b/src/test/model_evaluator.cpp
@@ -26,13 +26,19 @@ void tst_model_evaluator() {
     expr_ref vB0(m.mk_var(0, m.mk_bool_sort()), m);
     expr_ref vB1(m.mk_var(1, m.mk_bool_sort()), m);
     expr_ref vB2(m.mk_var(2, m.mk_bool_sort()), m);
-    expr_ref f01(m.mk_app(f, vI0, vB1), m);
-    expr_ref g01(m.mk_app(g, vI0, vB1), m);
-    expr_ref h01(m.mk_app(h, vI0, vB1), m);
+    expr* vI0p = vI0.get();
+    expr* vI1p = vI1.get();
+    expr* vB0p = vB0.get();
+    expr* vB1p = vB1.get();
+    expr* vB2p = vB2.get();
+
+    expr_ref f01(m.mk_app(f, vI0p, vB1p), m);
+    expr_ref g01(m.mk_app(g, vI0p, vB1p), m);
+    expr_ref h01(m.mk_app(h, vI0p, vB1p), m);
     func_interp* fi = alloc(func_interp, m, 2);
     func_interp* gi = alloc(func_interp, m, 2);
     func_interp* hi = alloc(func_interp, m, 2);
-    hi->set_else(m.mk_ite(vB1, m.mk_app(f, vI0, vB1), m.mk_app(g, vI0, vB1)));
+    hi->set_else(m.mk_ite(vB1p, m.mk_app(f, vI0p, vB1p), m.mk_app(g, vI0p, vB1p)));
     mdl.register_decl(h, hi);
     
 
@@ -42,23 +48,23 @@ void tst_model_evaluator() {
 
     {
         symbol nI("N");
-        fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(F, vI1, vB2))), vI0, a.mk_int(1)));
-        gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(G, vI1, vB2))), a.mk_int(2), vI0));
+        fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(F, vI1p, vB2p))), vI0p, a.mk_int(1)));
+        gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(G, vI1p, vB2p))), a.mk_int(2), vI0p));
         mdl.register_decl(g, gi);
         mdl.register_decl(f, fi);
         model_pp(std::cout, mdl);
-        e = m.mk_app(h, vI0, vB1);
+        e = m.mk_app(h, vI0p, vB1p);
         eval(e, v);
         std::cout << e << " " << v << "\n";
     }
 
     {
-        fi->set_else(m.mk_app(F, vI0, vB1));
-        gi->set_else(m.mk_app(G, vI0, vB1));
+        fi->set_else(m.mk_app(F, vI0p, vB1p));
+        gi->set_else(m.mk_app(G, vI0p, vB1p));
         mdl.register_decl(g, gi);
         mdl.register_decl(h, hi);
         model_pp(std::cout, mdl);
-        e = m.mk_app(h, vI0, vB1);
+        e = m.mk_app(h, vI0p, vB1p);
         eval(e, v);
         std::cout << e << " " << v << "\n";
     }