From 4f7b6a2f1801076f89fb1e5f44729b5419136255 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 9 Feb 2018 10:55:31 -0800
Subject: [PATCH] fix missing clear of weights

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 259b1550a..607335055 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -481,6 +481,7 @@ namespace sat {
             w2 = m_weights[(~l).index()];
             if (w1 >= w2) {
                 if (w2 >= k) {
+                    for (literal l2 : lits) m_weights[l2.index()] = 0;
                     // constraint is true
                     return;
                 }
@@ -2614,8 +2615,8 @@ namespace sat {
 
         // pre-condition is that the literals, except c.lit(), in c are unwatched.
         if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n";
-        // IF_VERBOSE(0, verbose_stream() << "re: " << c << "\n";);
         m_weights.resize(2*s().num_vars(), 0);
+
         for (literal l : c) {
             ++m_weights[l.index()];
         }