mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

fix missing clear of weights

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-09 10:55:31 -08:00
parent 5206e29bdd
commit 4f7b6a2f18
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/ba_solver.cpp
View file

@ -481,6 +481,7 @@ namespace sat {
w2 = m_weights[(~l).index()]; w2 = m_weights[(~l).index()];
if (w1 >= w2) { if (w1 >= w2) {
if (w2 >= k) { if (w2 >= k) {
for (literal l2 : lits) m_weights[l2.index()] = 0;
// constraint is true // constraint is true
return; return;
} }
@ -2614,8 +2615,8 @@ namespace sat {
// pre-condition is that the literals, except c.lit(), in c are unwatched. // pre-condition is that the literals, except c.lit(), in c are unwatched.
if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n"; 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); m_weights.resize(2*s().num_vars(), 0);
for (literal l : c) { for (literal l : c) {
++m_weights[l.index()]; ++m_weights[l.index()];
} }