From 4a1d76cf49cddf177f9e4ad503c26e170aa0e9f4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 23 Oct 2022 11:03:51 -0700
Subject: [PATCH] #6418 - add best-effort for nested and/or (from ite literals)

---
 src/qe/mbp/mbp_arith.cpp | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 9956a6d2e..e97eb4ef7 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -155,6 +155,35 @@ namespace mbp {
                 }
                 SASSERT(found_eq);
             }
+            else if (m.is_and(lit) && !is_not) {
+                fmls.append(to_app(lit)->get_num_args(), to_app(lit)->get_args());
+                return true;
+            }
+            else if (m.is_or(lit) && is_not) {
+                for (expr* arg : *to_app(lit))
+                    fmls.push_back(mk_not(m, arg));
+                return true;
+            }
+            else if (m.is_or(lit) && !is_not) {
+                for (expr* arg : *to_app(lit)) {
+                    if (eval.is_true(arg)) {
+                        fmls.push_back(arg);
+                        return true;
+                    }
+                }
+                TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";);
+                return false;
+            }
+            else if (m.is_and(lit) && is_not) {
+                for (expr* arg : *to_app(lit)) {
+                    if (eval.is_false(arg)) {
+                        fmls.push_back(mk_not(m, arg));
+                        return true;
+                    }
+                }
+                TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";);
+                return false;
+            }
             else {
                 TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";);
                 return false;