diff --git a/src/ast/pp.cpp b/src/ast/pp.cpp
index e307989c9..091b50c97 100644
--- a/src/ast/pp.cpp
+++ b/src/ast/pp.cpp
@@ -66,7 +66,6 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
     bool     single_line   = p.single_line();
 
     unsigned pos = 0;
-    unsigned ribbon_pos = 0;
     unsigned line = 0;
     unsigned len;
     unsigned i;
@@ -92,7 +91,6 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
                 break;
             }
             pos += len;
-            ribbon_pos += len;
             out << f->get_decl()->get_parameter(0).get_symbol();
             break;
         case OP_INDENT:
@@ -121,7 +119,6 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
                 break;
             }
             pos = indent;
-            ribbon_pos = 0;
             line++;
             if (line < max_num_lines) {
                 out << "\n";
diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index 0f1956a2b..060c2b1b9 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -546,6 +546,7 @@ bool emonics::invariant() const {
                 }
                 CTRACE("nla_solver_mons", !found, tout << "not found v" << v << ": " << m << "\n";);
                 SASSERT(found);
+                (void)found;
                 c = c->m_next;
             }
             while (c != ht.m_head);
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 5c6d0f311..2d9b1ccae 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -566,14 +566,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
     bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case, bool& are_unique) {
         SASSERT(m_ar.is_array(a));
-        bool are_values = true;
         are_unique = true;
         TRACE("model_evaluator", tout << mk_pp(a, m) << "\n";);
 
         while (m_ar.is_store(a)) {
             expr_ref_vector store(m);
             store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
-            are_values &= args_are_values(store, are_unique);
+            args_are_values(store, are_unique);
             stores.push_back(store);
             a = to_app(a)->get_arg(0);
         }
@@ -584,9 +583,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
         }
 
         if (m_ar_rw.has_index_set(a, else_case, stores)) {
-            for (auto const& store : stores) {
-                are_values &= args_are_values(store, are_unique);
-            }
+            for (auto const& store : stores) 
+                args_are_values(store, are_unique);
             return true;
         }
         if (!m_ar.is_as_array(a)) {
diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp
index f7b8f2797..97e0e3d72 100644
--- a/src/nlsat/nlsat_evaluator.cpp
+++ b/src/nlsat/nlsat_evaluator.cpp
@@ -286,22 +286,23 @@ namespace nlsat {
             }
             
             bool check_invariant() const {
-                SASSERT(m_sections.size() == m_sorted_sections.size());
-                for (unsigned i = 0; i < m_sorted_sections.size(); i++) {
-                    SASSERT(m_sorted_sections[i] < m_sections.size());
-                    SASSERT(m_sections[m_sorted_sections[i]].m_pos == i);
-                }
-                unsigned total_num_sections = 0;
-                unsigned total_num_signs = 0;
-                for (unsigned i = 0; i < m_info.size(); i++) {
-                    SASSERT(m_info[i].m_first_section <= m_poly_sections.size());
-                    SASSERT(m_info[i].m_num_roots == 0 || m_info[i].m_first_section < m_poly_sections.size());
-                    SASSERT(m_info[i].m_first_sign < m_poly_signs.size());
-                    total_num_sections += m_info[i].m_num_roots;
-                    total_num_signs += m_info[i].m_num_roots + 1;
-                }
-                SASSERT(total_num_sections == m_poly_sections.size());
-                SASSERT(total_num_signs == m_poly_signs.size());
+                DEBUG_CODE(
+                    SASSERT(m_sections.size() == m_sorted_sections.size());
+                    for (unsigned i = 0; i < m_sorted_sections.size(); i++) {
+                        SASSERT(m_sorted_sections[i] < m_sections.size());
+                        SASSERT(m_sections[m_sorted_sections[i]].m_pos == i);
+                    }
+                    unsigned total_num_sections = 0;
+                    unsigned total_num_signs = 0;
+                    for (unsigned i = 0; i < m_info.size(); i++) {
+                        SASSERT(m_info[i].m_first_section <= m_poly_sections.size());
+                        SASSERT(m_info[i].m_num_roots == 0 || m_info[i].m_first_section < m_poly_sections.size());
+                        SASSERT(m_info[i].m_first_sign < m_poly_signs.size());
+                        total_num_sections += m_info[i].m_num_roots;
+                        total_num_signs += m_info[i].m_num_roots + 1;
+                    }
+                    SASSERT(total_num_sections == m_poly_sections.size());
+                    SASSERT(total_num_signs == m_poly_signs.size()););
                 return true;
             }