From 1be692002d1da07a6e2b1a29bf1a23f38d94c0f4 Mon Sep 17 00:00:00 2001
From: Hari Govind V K <hgvk94@gmail.com>
Date: Wed, 16 Aug 2023 13:07:30 -0400
Subject: [PATCH] split on all ite terms. fix #6852 (#6859)

---
 src/qe/mbp/mbp_basic_tg.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/qe/mbp/mbp_basic_tg.cpp b/src/qe/mbp/mbp_basic_tg.cpp
index ee83012a7..70d25d89b 100644
--- a/src/qe/mbp/mbp_basic_tg.cpp
+++ b/src/qe/mbp/mbp_basic_tg.cpp
@@ -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;