From a7972204843deaa706b79246d95d41dc58421ad2 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 23 Oct 2023 15:27:12 +0200
Subject: [PATCH] fix

---
 src/math/polysat/superposition.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/math/polysat/superposition.cpp b/src/math/polysat/superposition.cpp
index f4049add9..f5590bdda 100644
--- a/src/math/polysat/superposition.cpp
+++ b/src/math/polysat/superposition.cpp
@@ -69,6 +69,8 @@ namespace polysat {
                 continue;
             if (!c1.is_pos_eq())
                 continue;
+            if (!c1.is_currently_true(s))  // may happen if value of 'v' was propagated by slicing, thus falsifying c1 (which then is the conflict constraint)
+                continue;
             SASSERT(c1.is_currently_true(s));
             SASSERT(c2.is_currently_false(s));
             SASSERT_EQ(c1.bvalue(s), l_true);