mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

Remove dead comment

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-14 06:36:44 -07:00
parent 1902360361
commit bbd917a0e6
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/ba_solver.cpp
View file

@ -527,14 +527,12 @@ namespace sat {
bool ba_solver::init_watch(pb& p) { bool ba_solver::init_watch(pb& p) {
clear_watch(p); clear_watch(p);
if (p.lit() != null_literal && value(p.lit()) == l_false) { if (p.lit() != null_literal && value(p.lit()) == l_false) {
//IF_VERBOSE(0, verbose_stream() << "negate: " << p.k() << "\n");
p.negate(); p.negate();
} }
VERIFY(p.lit() == null_literal || value(p.lit()) == l_true); VERIFY(p.lit() == null_literal || value(p.lit()) == l_true);
unsigned sz = p.size(), bound = p.k(); unsigned sz = p.size(), bound = p.k();
//IF_VERBOSE(0, verbose_stream() << "bound: " << p.k() << "\n");
// put the non-false literals into the head. // put the non-false literals into the head.
unsigned slack = 0, slack1 = 0, num_watch = 0, j = 0; unsigned slack = 0, slack1 = 0, num_watch = 0, j = 0;
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {