mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix #7311

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-07-27 08:26:42 +02:00
parent 1e6b13741c
commit 5f6bb3db3e
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/nlsat/nlsat_simplify.cpp
View file

@ -141,6 +141,8 @@ namespace nlsat {
auto& a = *to_ineq_atom(a1); auto& a = *to_ineq_atom(a1);
if (a.size() != 2) if (a.size() != 2)
continue; continue;
if (a.is_root_atom())
continue;
auto* p = a.p(0); auto* p = a.p(0);
auto* q = a.p(1); auto* q = a.p(1);
@ -229,6 +231,10 @@ namespace nlsat {
} }
break; break;
} }
default:
SASSERT(a.is_root_atom());
UNREACHABLE();
break;
} }
IF_VERBOSE(3, IF_VERBOSE(3,
s.display(verbose_stream(), c) << " ->\n"; s.display(verbose_stream(), c) << " ->\n";