mute some compiler warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Feb 3, 2024 · bc70282 · bc70282
1 parent 9425c41
commit bc70282
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 10 deletions.
diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp
@@ -525,9 +525,10 @@ namespace euf {
                     m_offsets.reserve(n->get_root_id() + 1);
                     m_offsets[n->get_root_id()].reset();
                 }
-                for (auto const& off : m_offsets) {
-                    SASSERT(off.empty());
-                }
+                DEBUG_CODE(
+                    for (auto const& off : m_offsets) {
+                        VERIFY(off.empty());
+                    });
                 m_jtodo.reset();
                 return;
             }

diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
@@ -545,16 +545,9 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
     bool simp     = false;
     bool modified = false;
     bool forward  = true;
-    unsigned rounds = 0;
     expr* narg;
 
     while (true) {
-        rounds++;
-#if 0
-        if (rounds > 10)
-            verbose_stream() << "rounds: " << rounds << "\n";
-#endif
-
 
 #define PROCESS_ARG()                                                                           \
         {                                                                                       \

diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
@@ -3624,6 +3624,7 @@ namespace polynomial {
 
             unsigned counter = 0;
             while (true) {
+                (void)counter;
                 SASSERT(degree(pp_u, x) >= degree(pp_v, x));
                 unsigned delta = degree(pp_u, x) - degree(pp_v, x);
                 TRACE("polynomial_gcd_detail",
@@ -4169,6 +4170,7 @@ namespace polynomial {
             unsigned counter   = 0;
 
             for (;; counter++) {
+                (void) counter;
                 while (true) {
                     peek_fresh(interpolator.inputs(), p, val);
                     // the selected value must satisfy lc_g(val) != 0