#6299

Z3Prover · Aug 25, 2022 · 6c165e8 · 6c165e8
1 parent f6e151a
commit 6c165e8
Showing 1 changed file with 10 additions and 1 deletion.
diff --git a/src/qe/mbp/mbp_solve_plugin.cpp b/src/qe/mbp/mbp_solve_plugin.cpp
@@ -376,14 +376,23 @@ 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 {
                     return false;
                 }
                 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: