diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp
index 14fc594b6..3fdf96f87 100644
--- a/src/test/cnf_backbones.cpp
+++ b/src/test/cnf_backbones.cpp
@@ -38,6 +38,7 @@ static void STD_CALL on_ctrl_c(int) {
     raise(SIGINT);
 }
 
+#if 0
 static void display_model(sat::solver const & s) {
     sat::model const & m = s.get_model();
     for (unsigned i = 1; i < m.size(); i++) {
@@ -49,6 +50,7 @@ static void display_model(sat::solver const & s) {
     }
     std::cout << "\n";
 }
+#endif
 
 static void display_status(lbool r) {
     switch (r) {
diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp
index 99a0480a6..8a62dcb7d 100644
--- a/src/test/dl_context.cpp
+++ b/src/test/dl_context.cpp
@@ -15,11 +15,12 @@ using namespace datalog;
 
 
 void tst_dl_context() {
-    symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2")  };
 
     return;
 
 #if 0
+    symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2")  };
+
     const unsigned rel_cnt = sizeof(relations)/sizeof(symbol);
     const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog";
 
diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp
index 0bc9dfe3c..987d8e13b 100644
--- a/src/test/polynorm.cpp
+++ b/src/test/polynorm.cpp
@@ -89,6 +89,7 @@ private:
         expr_ref_vector& coefficients = poly.coefficients();
         expr_ref& coefficient = poly.coefficient();
         (void) coefficient;
+        (void) coefficients;
 
         m_rw(term);
 
@@ -171,7 +172,7 @@ static expr_ref mk_mul(arith_util& arith, unsigned num_args, expr* const* args)
 
 static void nf(expr_ref& term) {
     ast_manager& m = term.get_manager();
-    expr *e1, *e2;
+    expr *e1 = 0, *e2 = 0;
 
     th_rewriter rw(m);
     arith_util arith(m);
diff --git a/src/test/sat_user_scope.cpp b/src/test/sat_user_scope.cpp
index 54de5976a..a271ce6bb 100644
--- a/src/test/sat_user_scope.cpp
+++ b/src/test/sat_user_scope.cpp
@@ -34,11 +34,6 @@ static void add_clause(sat::solver& s, random_gen& r, trail_t& t) {
     s.mk_clause(cls.size(), cls.c_ptr());
 }
 
-static void display_state(std::ostream& out, sat::solver& s, trail_t& t) {
-    (void)t;
-    s.display(out);
-}
-
 static void pop_user_scope(sat::solver& s, trail_t& t) {
     std::cout << "pop\n";
     s.user_pop(1);
diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp
index 3d9815873..43aefed99 100644
--- a/src/test/upolynomial.cpp
+++ b/src/test/upolynomial.cpp
@@ -164,7 +164,7 @@ static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, m
         for (unsigned j = 0; j < roots.size(); j++) {
             if (to_rational(roots[j]) == r) {
                 SASSERT(!visited[j]);
-                SASSERT(!found);
+                VERIFY(!found);
                 found = true;
                 visited[j] = true;
             }
@@ -172,7 +172,7 @@ static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, m
         for (unsigned j = 0; j < lowers.size(); j++) {
             unsigned j_prime = j + roots.size();
             if (to_rational(lowers[j]) < r && r < to_rational(uppers[j])) {
-                SASSERT(!found);
+                VERIFY(!found);
                 SASSERT(!visited[j_prime]);
                 found = true;
                 visited[j_prime] = true;