From 8a23523f20dc49e1b474a0b6792609185daa4bf6 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 25 Mar 2024 13:20:24 +0100
Subject: [PATCH] fix crash on EBxzQox7raUO.smt2

---
 src/sat/smt/polysat/project_interval.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/sat/smt/polysat/project_interval.cpp b/src/sat/smt/polysat/project_interval.cpp
index 7f1404527..e3b5cc6ff 100644
--- a/src/sat/smt/polysat/project_interval.cpp
+++ b/src/sat/smt/polysat/project_interval.cpp
@@ -131,6 +131,12 @@ namespace polysat {
                     break;
                 if (m_fixed[i].length != m_fixed[j].length)
                     break;
+                if (m_fixed[i].value != m_fixed[j].value) {
+                    // same subslice, but with different values;
+                    // this should not happen in a fully saturated egraph (wrt. bv_plugin).
+                    break;
+                }
+                VERIFY(m_fixed[j].child != null_var);
                 SASSERT(m_fixed[i].value == m_fixed[j].value);
                 i = j;