mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
mute some compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9425c419ad
commit
bc70282a18
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -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() \
|
||||
{ \
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue