mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
change assert to conditional code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7714bff6b2
commit
58cc69ca61
|
@ -839,7 +839,7 @@ namespace smt {
|
|||
|
||||
void mk_ite_cnstr(app * n);
|
||||
|
||||
void dec_ref(literal l) { SASSERT(m_lit_occs[l.index()] > 0); m_lit_occs[l.index()]--; }
|
||||
void dec_ref(literal l) { if (m_lit_occs[l.index()] > 0) m_lit_occs[l.index()]--; }
|
||||
|
||||
void inc_ref(literal l) { m_lit_occs[l.index()]++; }
|
||||
|
||||
|
|
|
@ -1373,6 +1373,15 @@ namespace smt {
|
|||
break;
|
||||
}
|
||||
TRACE("mk_clause", tout << "after simplification:\n"; display_literals_verbose(tout, num_lits, lits) << "\n";);
|
||||
#if 0
|
||||
for (unsigned i = 0; i < num_lits; ++i) {
|
||||
expr_ref tmp(m);
|
||||
literal2expr(lits[i], tmp);
|
||||
std::cout << tmp << "\n";
|
||||
}
|
||||
std::cout << "\n";
|
||||
#endif
|
||||
|
||||
unsigned activity = 0;
|
||||
if (activity == 0)
|
||||
activity = 1;
|
||||
|
|
Loading…
Reference in a new issue