From f51b194017f14f264297bef48039ecf5c1276821 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 7 Nov 2023 13:14:47 +0100
Subject: [PATCH] remove overly strict assertion

---
 src/math/polysat/saturation.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index fb67a043e..30ada37e7 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -129,7 +129,6 @@ namespace polysat {
                 continue;
             if (!i.as_signed_constraint().contains_var(y))
                 continue;
-            SASSERT_EQ(s.get_level(y), s.get_level(x));  // propagated by slicing egraph since they are equivalent
             SASSERT(s.m_search.get_pvar_index(y) < s.m_search.get_pvar_index(x));  // y was the earlier one since we are currently resolving x
             pdd const lhs = i.lhs().subst_pdd(x, s.var(y));
             pdd const rhs = i.rhs().subst_pdd(x, s.var(y));