mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 16:38:45 +00:00
Code Activity

assertion fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-29 19:53:22 -07:00
parent d6327d69d2
commit 133f376172
3 changed files with 15 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/sat/ba_solver.cpp
View file

@ -634,8 +634,9 @@ namespace sat {
exit(0); exit(0);
return l_undef; return l_undef;
} }
SASSERT(validate_watch(p)); validate_watch(p);
// SASSERT(validate_watch(p));
SASSERT(index < num_watch); SASSERT(index < num_watch);
unsigned index1 = index + 1; unsigned index1 = index + 1;
@ -710,6 +711,8 @@ namespace sat {
} }
} }
validate_watch(p);
TRACE("sat", display(tout << "assign: " << alit << "\n", p, true);); TRACE("sat", display(tout << "assign: " << alit << "\n", p, true););
BADLOG(verbose_stream() << "unwatch " << alit << " watch: " << p.num_watch() << " size: " << p.size() << " slack: " << p.slack() << " " << inconsistent() << "\n"); BADLOG(verbose_stream() << "unwatch " << alit << " watch: " << p.num_watch() << " size: " << p.size() << " slack: " << p.slack() << " " << inconsistent() << "\n");
@ -3428,7 +3431,9 @@ namespace sat {
} }
bool ba_solver::validate_unit_propagation(pb const& p, literal alit) const { bool ba_solver::validate_unit_propagation(pb const& p, literal alit) const {
if (p.lit() != null_literal && value(p.lit()) != l_true) return false; if (p.lit() != null_literal && value(p.lit()) != l_true) {
return false;
}
unsigned sum = 0; unsigned sum = 0;
TRACE("sat", display(tout << "validate: " << alit << "\n", p, true);); TRACE("sat", display(tout << "validate: " << alit << "\n", p, true););
@ -3446,11 +3451,14 @@ namespace sat {
unsigned sum = 0; unsigned sum = 0;
// all elements of r are true, // all elements of r are true,
for (literal l : r) { for (literal l : r) {
if (value(l) != l_true) return false; if (value(l) != l_true) {
return false;
}
} }
// the sum of elements not in r or alit add up to less than k. // the sum of elements not in r or alit add up to less than k.
for (wliteral wl : p) { for (wliteral wl : p) {
if (wl.second != alit && !r.contains(~wl.second)) { literal lit = wl.second;
if (lit != alit && value(lit) != l_false && !r.contains(~lit)) {
sum += wl.first; sum += wl.first;
} }
} }

2
src/sat/sat_lookahead.cpp
View file

@ -1910,7 +1910,7 @@ namespace sat {
while (true) { while (true) {
lbool result = cube(lits); lbool result = cube(lits);
if (lits.empty() || result != l_undef) { if (lits.empty() || result != l_undef) {
return result; return l_undef;
} }
display_cube(std::cout, lits); display_cube(std::cout, lits);
} }

1
src/util/memory_manager.cpp
View file

@ -60,6 +60,7 @@ static void throw_out_of_memory() {
if (g_exit_when_out_of_memory) { if (g_exit_when_out_of_memory) {
std::cerr << g_out_of_memory_msg << "\n"; std::cerr << g_out_of_memory_msg << "\n";
__assume(0);
exit(ERR_MEMOUT); exit(ERR_MEMOUT);
} }
else { else {