Skip to content

Commit 8f42b45

Browse files
committed
Fixing debug printing
1 parent 54dd093 commit 8f42b45

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/counter.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1544,7 +1544,7 @@ FF Counter::check_count(const bool also_incl_curr_and_later_dec) {
15441544
*cube_cnt *= *get_weight(Lit(i+1, s2.get_model()[i] == CMSat::l_True));
15451545
}
15461546
}
1547-
VERBOSE_DEBUG_DO(cout << cube_cnt << " + ";);
1547+
VERBOSE_DEBUG_DO(cout << *cube_cnt << " + ";);
15481548
*cnt += *cube_cnt;
15491549
}
15501550

@@ -1597,7 +1597,7 @@ FF Counter::check_count(const bool also_incl_curr_and_later_dec) {
15971597
if (!diff->is_zero()) {
15981598
auto diff_ratio = diff->dup();
15991599
*diff_ratio /= *cnt;
1600-
debug_print("OOps, diff : " << diff << " diff ratio: " << *diff_ratio);
1600+
debug_print("OOps, diff : " << *diff << " diff ratio: " << *diff_ratio);
16011601
print_all_levels();
16021602
okay = false;
16031603
}

0 commit comments

Comments
 (0)