diff --git a/src/test/interval.cpp b/src/test/interval.cpp
index 64f6cb88c..289265949 100644
--- a/src/test/interval.cpp
+++ b/src/test/interval.cpp
@@ -200,14 +200,12 @@ static void mk_random_interval(T & cfg, interval & a, unsigned magnitude) {
 
 #define BUFFER_SZ 256
 static int g_problem_id = 0;
-static char g_buffer[BUFFER_SZ];
-static std::stringstream ous;
 
-char const * get_next_file_name() {
-    ous.clear();
+std::string get_next_file_name() {
+    std::stringstream ous;
     ous << "interval_lemma_" << g_problem_id << ".smt2";
     g_problem_id++;
-    return ous.str().c_str();
+    return ous.str();
 }
 
 static void display_lemmas(unsynch_mpq_manager & nm, char const * result_term,
diff --git a/src/test/no_overflow.cpp b/src/test/no_overflow.cpp
index dd826bad8..c7124a5ce 100644
--- a/src/test/no_overflow.cpp
+++ b/src/test/no_overflow.cpp
@@ -529,8 +529,8 @@ void test_div(unsigned bvsize) {
     Z3_del_context(ctx);
 }
 
-typedef Z3_ast (Z3_API *NO_OVFL_ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2, bool is_signed);
-typedef Z3_ast (Z3_API *ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2);
+typedef Z3_ast (*NO_OVFL_ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2, bool is_signed);
+typedef Z3_ast (*ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2);
 
 typedef enum { OVFL_FUNC, UDFL_FUNC } overflow_type;
 
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index 859d7f2e5..2e170979a 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -377,6 +377,9 @@ static void add_random_ineq(
     case opt::t_mod:
         NOT_IMPLEMENTED_YET();        
         break;        
+    default:
+        NOT_IMPLEMENTED_YET();        
+        break;                
     }
     fmls.push_back(fml);
     mbo.add_constraint(vars, rational(coeff), rel);