From bc70282a180e7d703bd15fd98ee0c4755619f015 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 3 Feb 2024 15:42:06 -0800
Subject: [PATCH] mute some compiler warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/euf/euf_bv_plugin.cpp      | 7 ++++---
 src/ast/rewriter/bool_rewriter.cpp | 7 -------
 src/math/polynomial/polynomial.cpp | 2 ++
 3 files changed, 6 insertions(+), 10 deletions(-)

diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp
index 1b32e9b3a..4b0cd6cfc 100644
--- 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
index 13a392d24..2176ff129 100644
--- 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
index 96a4a05ca..da6bc7b39 100644
--- 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