mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

remove verificaiton code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-08 16:07:58 -07:00
parent 10e4235b4c
commit f85c02600f
3 changed files with 0 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/ba_solver.cpp
View file

@ -1387,7 +1387,6 @@ namespace sat {
IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";); IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";);
return false; return false;
} }
if (m_lemma[0] == null_literal) { if (m_lemma[0] == null_literal) {
if (m_lemma.size() == 1) { if (m_lemma.size() == 1) {

1
src/sat/sat_elim_eqs.cpp
View file

@ -229,7 +229,6 @@ namespace sat {
cleanup_clauses(roots, m_solver.m_learned); cleanup_clauses(roots, m_solver.m_learned);
if (m_solver.inconsistent()) return; if (m_solver.inconsistent()) return;
save_elim(roots, to_elim); save_elim(roots, to_elim);
VERIFY(check_clauses(roots));
m_solver.propagate(false); m_solver.propagate(false);
SASSERT(check_clauses(roots)); SASSERT(check_clauses(roots));
} }

3
src/sat/sat_solver.cpp
View file

@ -372,9 +372,6 @@ namespace sat {
clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, bool learned) { clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, bool learned) {
m_stats.m_mk_clause++; m_stats.m_mk_clause++;
for (unsigned i = 0; i + 1 < num_lits; ++i) {
VERIFY (lits[i] != ~lits[i + 1]);
}
clause * r = m_cls_allocator.mk_clause(num_lits, lits, learned); clause * r = m_cls_allocator.mk_clause(num_lits, lits, learned);
SASSERT(!learned || r->is_learned()); SASSERT(!learned || r->is_learned());
bool reinit = attach_nary_clause(*r); bool reinit = attach_nary_clause(*r);