mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

split on all ite terms. fix #6852 (#6859)

Browse source
This commit is contained in:
Hari Govind V K 2023-08-16 13:07:30 -04:00 committed by GitHub
parent 50717fb655
commit 1be692002d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/qe/mbp/mbp_basic_tg.cpp
View file

@ -43,6 +43,8 @@ struct mbp_basic_tg::impl {
void mark_seen(expr *t) { m_seen.mark(t); }
bool is_seen(expr *t) { return m_seen.is_marked(t); }
//Split on all ite terms, irrespective of whether
//they contain variables/are c-ground
bool apply() {
if (!m_use_mdl) return false;
expr *term, *c, *th, *el;
@ -60,7 +62,6 @@ struct mbp_basic_tg::impl {
SASSERT(!m.is_implies(term));
if (is_seen(term)) continue;
if (m_tg.is_cgr(term)) continue;
if (m.is_ite(term, c, th, el)) {
mark_seen(term);
progress = true;