From 82798863ba4646fee3f7c1b4d218a444745da8d9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 21 Jan 2022 17:58:30 +0100
Subject: [PATCH] patch crash for bench0

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/explain.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 461f45c98..0b12155d9 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -164,6 +164,8 @@ namespace polysat {
             LOG("try-reduce is false " << c2.is_currently_false(s));
             if (!c2.is_currently_false(s))
                 continue;
+            if (c2.bvalue(s) == l_false)
+                return false;
             if (!c2->has_bvar() || l_undef == c2.bvalue(s)) {
                 vector<signed_constraint> premises;
                 premises.push_back(c);
@@ -174,10 +176,13 @@ namespace polysat {
             core.reset();
             LOG_H3("Polynomial superposition " << eq << " " << c << " reduced to " << c2);
             if (c2.bvalue(s) == l_false) {
+                UNREACHABLE();
+                // TODO this loops or crashes depending on whether we
+                // return true or false.
                 core.insert(eq);
                 core.insert(c);
                 core.insert(~c2);
-                return false;
+                return true;
             }
             core.set(c2);
             return true;