From bef1be8cb582685df965b1623ee9d30ebb7bb8cf Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 7 Oct 2022 10:11:00 +0200
Subject: [PATCH] should not happen anymore

---
 src/math/polysat/viable.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index fa10299af..074d1652e 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -706,6 +706,7 @@ namespace polysat {
         // TODO: should not be here, too general
         for (auto c : core) {
             if (c.bvalue(s) == l_false) {
+                UNREACHABLE();  // an invariant of the new conflict state is that bvalue of all inserted constraints is l_true (cf. assertion in conflict::insert)
                 core.set(~c);
                 core.logger().log("");
                 break;