diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index ab19a5586..930abe4e6 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -1081,6 +1081,7 @@ namespace seq {
         sort* domain[4] = { srt, srt, srt, srt };
         auto d = plugin.ensure_def(symbol("ra"), 4, domain, m.mk_bool_sort(), true);
         func_decl* ra = d.get_def()->get_decl();
+        (void)ra;
         sort* isrt = a.mk_int();
         var_ref vi(m.mk_var(5, isrt), m);
         var_ref vj(m.mk_var(4, isrt), m);
@@ -1089,6 +1090,7 @@ namespace seq {
         var_ref vt(m.mk_var(1, srt), m);
         var_ref vr(m.mk_var(0, srt), m);
         var* vars[6] = { vi, vj, vs, vp, vt, vr };
+        (void)vars;
         expr_ref len_s(seq.str.mk_length(vs), m);
         expr_ref len_r(seq.str.mk_length(vr), m);
         expr_ref test1(m.mk_eq(len_s, vi), m);
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index 5d00d8a6b..0261ad979 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -268,6 +268,7 @@ namespace qe {
         ap.set_check_purified(false);
         vector<mbp::def> defs;
         bool ok = ap.project(*mdl.get(), avars, lits, defs);
+        (void)ok;
         CTRACE("qe", !ok, tout << "projection failure ignored!!!!\n");
         return defs;
     }
diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp
index 5e1a76b9f..e1d0d4b33 100644
--- a/src/sat/smt/array_internalize.cpp
+++ b/src/sat/smt/array_internalize.cpp
@@ -77,7 +77,8 @@ namespace array {
 
     bool solver::post_visit(expr* e, bool sign, bool root) {
         euf::enode* n = expr2enode(e);
-        app* a = to_app(e);        
+        app *a = to_app(e);
+        (void)a;
         SASSERT(!n || !n->is_attached_to(get_id()));
         if (!n) 
             n = mk_enode(e, false);