From 5f6bb3db3e3fd054f42ee1382bab1152f4b86a5c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 27 Jul 2024 08:26:42 +0200
Subject: [PATCH] fix #7311
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/nlsat/nlsat_simplify.cpp | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/src/nlsat/nlsat_simplify.cpp b/src/nlsat/nlsat_simplify.cpp
index 8148d721f..2901d22c2 100644
--- a/src/nlsat/nlsat_simplify.cpp
+++ b/src/nlsat/nlsat_simplify.cpp
@@ -141,6 +141,8 @@ namespace nlsat {
auto& a = *to_ineq_atom(a1);
if (a.size() != 2)
continue;
+ if (a.is_root_atom())
+ continue;
auto* p = a.p(0);
auto* q = a.p(1);
@@ -229,6 +231,10 @@ namespace nlsat {
}
break;
}
+ default:
+ SASSERT(a.is_root_atom());
+ UNREACHABLE();
+ break;
}
IF_VERBOSE(3,
s.display(verbose_stream(), c) << " ->\n";