fix #7311

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Jul 27, 2024 · 5f6bb3d · 5f6bb3d
1 parent 1e6b137
commit 5f6bb3d
Showing 1 changed file with 6 additions and 0 deletions.
diff --git 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";