From 42de2743076723171b91d9ec17cbd8468398a88a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Oct 2017 07:49:20 -0700 Subject: [PATCH] bug fixes Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 1dbaefbce..6a68c30c9 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -221,6 +221,7 @@ namespace sat { literal root = c.lit(); if (root != null_literal && root.sign() == is_true) { c.negate(); + root.neg(); } if (root != null_literal) { if (!is_watched(root, c)) watch_literal(root, c); @@ -1563,10 +1564,6 @@ namespace sat { watch_literal(~lit, *c); } SASSERT(c->well_formed()); - if (c->id() == 1344) { - std::cout << "is watched: " << lit << " " << is_watched(lit, *c) << "\n"; - std::cout << "is watched: " << ~lit << " " << is_watched(~lit, *c) << "\n"; - } } @@ -1987,17 +1984,10 @@ namespace sat { } void ba_solver::unwatch_literal(literal lit, constraint& c) { - if (c.index() == 1344) { - std::cout << "unwatch: " << lit << "\n"; - } get_wlist(~lit).erase(watched(c.index())); } void ba_solver::watch_literal(literal lit, constraint& c) { - if (c.index() == 1344) { - std::cout << "watch: " << lit << "\n"; - } - get_wlist(~lit).push_back(watched(c.index())); }