mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix build warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a0892c6669
commit
d0f2b00f96
|
@ -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<table_kind>(GET_TAG(t))) {
|
||||
case UNARY:
|
||||
UNTAG(unary_table*, t)->erase(n);
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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)
|
||||
|
|
Loading…
Reference in a new issue