From 133f3761727f7791a4aea3f46b9488d85036338a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 29 Sep 2017 19:53:22 -0700
Subject: [PATCH] assertion fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp       | 18 +++++++++++++-----
 src/sat/sat_lookahead.cpp   |  2 +-
 src/util/memory_manager.cpp |  1 +
 3 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index e8f97ce5e..a4275f804 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -634,8 +634,9 @@ namespace sat {
             exit(0);
             return l_undef;
         }
-
-        SASSERT(validate_watch(p));
+        
+        validate_watch(p);
+        // SASSERT(validate_watch(p));
         
         SASSERT(index < num_watch);
         unsigned index1 = index + 1;
@@ -710,6 +711,8 @@ namespace sat {
             }
         }
 
+        validate_watch(p);
+
         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");
@@ -3428,7 +3431,9 @@ namespace sat {
     }
 
     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;
         TRACE("sat", display(tout << "validate: " << alit << "\n", p, true););
@@ -3446,11 +3451,14 @@ namespace sat {
         unsigned sum = 0;
         // all elements of r are true, 
         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.
         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;
             }
         }
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 92ba7b808..596b9abe7 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -1910,7 +1910,7 @@ namespace sat {
         while (true) {
             lbool result = cube(lits);
             if (lits.empty() || result != l_undef) {
-                return result;
+                return l_undef;
             }
             display_cube(std::cout, lits);
         }
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 08fada396..0b394b450 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -60,6 +60,7 @@ static void throw_out_of_memory() {
 
     if (g_exit_when_out_of_memory) {
         std::cerr << g_out_of_memory_msg << "\n";
+        __assume(0);
         exit(ERR_MEMOUT);
     }
     else {