mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
unused / return warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
13e335f062
commit
f5164d166b
|
@ -81,6 +81,7 @@ namespace dd {
|
|||
}
|
||||
}
|
||||
SASSERT(well_formed());
|
||||
return 0;
|
||||
}
|
||||
|
||||
bool pdd_manager::check_result(op_entry*& e1, op_entry const* e2, PDD a, PDD b, PDD c) {
|
||||
|
@ -231,6 +232,7 @@ namespace dd {
|
|||
}
|
||||
}
|
||||
SASSERT(well_formed());
|
||||
return pdd(zero_pdd, this);
|
||||
}
|
||||
|
||||
pdd_manager::PDD pdd_manager::minus_rec(PDD a) {
|
||||
|
|
|
@ -155,7 +155,7 @@ namespace sat {
|
|||
p.set_uint("sat.max_conflicts", 10000);
|
||||
p.set_bool("sat.binspr", false);
|
||||
s->updt_params(p);
|
||||
lbool r = s->check(0, nullptr);
|
||||
s->check(0, nullptr);
|
||||
}
|
||||
|
||||
if (s->inconsistent()) {
|
||||
|
@ -422,7 +422,6 @@ namespace sat {
|
|||
break;
|
||||
}
|
||||
}
|
||||
bool first = m_state == ~0;
|
||||
m_state &= mask;
|
||||
TRACE("sat",
|
||||
{
|
||||
|
|
Loading…
Reference in a new issue