mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 09:20:22 +00:00
Code Activity

assert

Browse source
This commit is contained in:
Jakob Rath 2023-10-23 15:25:24 +02:00
parent c87aa8bcf8
commit 25d1bca583
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/slicing.cpp
View file

@ -549,6 +549,7 @@ namespace polysat {
} }
bool slicing::is_value(enode* n) const { bool slicing::is_value(enode* n) const {
SASSERT(n);
SASSERT(is_app(n->get_expr())); // we only create app nodes at the moment; if this fails just return false here. SASSERT(is_app(n->get_expr())); // we only create app nodes at the moment; if this fails just return false here.
app* a = n->get_app(); app* a = n->get_app();
return a->get_num_args() == 1 && m_bv->is_numeral(a->get_arg(0)); return a->get_num_args() == 1 && m_bv->is_numeral(a->get_arg(0));