From 6c165e89dcc88da56f7fdc8a51349478f0574947 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 24 Aug 2022 20:25:01 -0700
Subject: [PATCH] #6299

---
 src/qe/mbp/mbp_solve_plugin.cpp | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/qe/mbp/mbp_solve_plugin.cpp b/src/qe/mbp/mbp_solve_plugin.cpp
index c43fa402f0b..d80a3665d15 100644
--- a/src/qe/mbp/mbp_solve_plugin.cpp
+++ b/src/qe/mbp/mbp_solve_plugin.cpp
@@ -376,7 +376,7 @@ namespace mbp {
                     rhs = m_bv.mk_concat(2, args);
                 }
                 else if (lo > 0 && hi + 1 == sz) {
-                    expr* args[3] = { rhs, m_bv.mk_extract(lo - 1, 0, e) };
+                    expr* args[2] = { rhs, m_bv.mk_extract(lo - 1, 0, e) };
                     rhs = m_bv.mk_concat(2, args);                    
                 }
                 else {
@@ -384,6 +384,15 @@ namespace mbp {
                 }
                 return true;
             }
+#if 0
+            expr *f = nullptr
+            // this one is for Nuno to find and generalize for invertible expressions
+            if (m_bv.is_bv_add(lhs, e, f) && is_variable(e)) {
+                lhs = e;
+                rhs = m_bv.mk_bv_sub(rhs, f);
+                return true;
+            }
+#endif
             return false;
         }
     public: