diff --git a/src/ast/rewriter/factor_equivs.cpp b/src/ast/rewriter/factor_equivs.cpp
index 6384ad8ce..e06c9479c 100644
--- a/src/ast/rewriter/factor_equivs.cpp
+++ b/src/ast/rewriter/factor_equivs.cpp
@@ -76,7 +76,7 @@ void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
  */
 expr *choose_rep(expr_equiv_class::eq_class &clazz, ast_manager &m) {
     expr *rep = nullptr;
-    unsigned rep_sz, elem_sz;
+    unsigned rep_sz = 0, elem_sz;
     for (expr *elem : clazz) {
         if (!m.is_value(elem)) {
             elem_sz = get_num_exprs(elem);
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index d8cb31486..35b9bd9bb 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -3112,7 +3112,6 @@ namespace smt2 {
 
         sexpr_ref parse_sexpr_ref() {
             m_num_bindings    = 0;
-            unsigned found_errors = 0;
             m_num_open_paren = 0;
 
             try {
diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp
index 3f62a8998..f21e54fb7 100644
--- a/src/sat/sat_ddfw.cpp
+++ b/src/sat/sat_ddfw.cpp
@@ -561,22 +561,23 @@ namespace sat {
             IF_VERBOSE(0, if (v_reward != reward(v)) verbose_stream() << v << " " << v_reward << " " << reward(v) << "\n");
             SASSERT(reward(v) == v_reward);
         }
-        for (auto const& ci : m_clauses) {
-            SASSERT(ci.m_weight > 0);
-        }
-        for (unsigned i = 0; i < m_clauses.size(); ++i) {
-            bool found = false;
-            for (literal lit : get_clause(i)) {
-                if (is_true(lit)) found = true;
+        DEBUG_CODE(
+            for (auto const& ci : m_clauses) {
+                SASSERT(ci.m_weight > 0);
             }
-            SASSERT(found == !m_unsat.contains(i));
-        }
-        // every variable in a false clause is in unsat vars
-        for (unsigned cl : m_unsat) {
-            for (literal lit : get_clause(cl)) {
-                SASSERT(m_unsat_vars.contains(lit.var()));
+            for (unsigned i = 0; i < m_clauses.size(); ++i) {
+                bool found = false;
+                for (literal lit : get_clause(i)) {
+                    if (is_true(lit)) found = true;
+                }
+                SASSERT(found == !m_unsat.contains(i));
             }
-        }
+            // every variable in a false clause is in unsat vars
+            for (unsigned cl : m_unsat) {
+                for (literal lit : get_clause(cl)) {
+                    SASSERT(m_unsat_vars.contains(lit.var()));
+                }
+            });
     }
 
     void ddfw::updt_params(params_ref const& _p) {