From d0f2b00f96e0549a69fd9a71b0d3f9c05d99e8a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Jul 2023 12:24:30 -0700 Subject: [PATCH] fix build warnings Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_etable.cpp | 5 ----- src/sat/sat_ddfw.cpp | 2 +- src/sat/smt/arith_diagnostics.cpp | 3 +++ 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp index 17be983fe..d79944c9b 100644 --- a/src/ast/euf/euf_etable.cpp +++ b/src/ast/euf/euf_etable.cpp @@ -224,11 +224,6 @@ namespace euf { void etable::erase(enode * n) { SASSERT(n->num_args() > 0); void * t = get_table(n); - static unsigned count = 0; - //verbose_stream() << "erase " << (++count) << " " << n << "\n"; - // if (count == 10398) { - // verbose_stream() << "here\n"; - // } switch (static_cast(GET_TAG(t))) { case UNARY: UNTAG(unary_table*, t)->erase(n); diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp index ca274be51..f15c241f2 100644 --- a/src/sat/sat_ddfw.cpp +++ b/src/sat/sat_ddfw.cpp @@ -494,7 +494,7 @@ namespace sat { unsigned h = value_hash(); unsigned occs = 0; bool contains = m_models.find(h, occs); - if (!m_models.contains(h)) { + if (!contains) { for (unsigned v = 0; v < num_vars(); ++v) bias(v) += value(v) ? 1 : -1; if (m_models.size() > m_config.m_max_num_models) diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp index 783f268bd..e621ee9d7 100644 --- a/src/sat/smt/arith_diagnostics.cpp +++ b/src/sat/smt/arith_diagnostics.cpp @@ -199,6 +199,9 @@ namespace arith { name = "implied-eq"; args.push_back(arith.mk_int(m_num_le)); break; + default: + name = "unknown-arithmetic"; + break; } rational lc(1); for (unsigned i = m_lit_head; i < m_lit_tail; ++i)