From d95e167d6181ef8eef48cba3f552dd58f2b9287c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 21 May 2018 16:53:33 -0700
Subject: [PATCH] updates to mbqi

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/extra_cmds/dbg_cmds.cpp |  2 +-
 src/qe/qe_arrays.cpp                    | 34 ++++++++++++++++++++++++-
 2 files changed, 34 insertions(+), 2 deletions(-)

diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index 1b378f430..ceb979761 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -369,7 +369,7 @@ public:
     void set_next_arg(cmd_context & ctx, unsigned num, expr * const * ts) override {
         m_vars.append(num, ts);
     }
-    void prepare(cmd_context & ctx) override { m_fml = nullptr; }
+    void prepare(cmd_context & ctx) override { m_fml = nullptr; m_vars.reset(); }
     void execute(cmd_context & ctx) override { 
         ast_manager& m = ctx.m();
         app_ref_vector vars(m);
diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index cc3952457..f7b8898c1 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -1214,7 +1214,39 @@ namespace qe {
             for (unsigned j = 0; j < n; ++j) {
                 lits.push_back(m.mk_eq(x.m_vars[j], y.m_vars[j]));
             }
-        }        
+        }
+        
+        bool solve_eq(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+            // find an equality to solve for.
+            expr* s, *t;
+            for (unsigned i = 0; i < lits.size(); ++i) {
+                if (m.is_eq(lits[i].get(), s, t)) {
+                    vector<indices> idxs;
+                    expr_ref save(m), back(m);
+                    save = lits[i].get();
+                    back = lits.back();
+                    lits[i] = back;
+                    lits.pop_back();
+                    unsigned sz = lits.size();
+                    if (contains_x(s) && !contains_x(t) && is_app(s)) {
+                        if (solve(model, to_app(s), t, idxs, vars, lits)) {
+                            return true;
+                        }
+                    }
+                    else if (contains_x(t) && !contains_x(s) && is_app(t)) {
+                        if (solve(model, to_app(t), s, idxs, vars, lits)) {
+                            return true;
+                        }
+                    }
+                    // put back the equality literal.
+                    lits.resize(sz);
+                    lits.push_back(back);
+                    lits[i] = save;
+                }
+                // TBD: not distinct?
+            }
+            return false;
+        }
 
         bool solve(model& model, app* s, expr* t, vector<indices>& idxs, app_ref_vector& vars, expr_ref_vector& lits) {
             SASSERT(contains_x(s));