From bef509b02e19f0f326b3a46449bab975c8b832f3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 25 Feb 2019 19:20:35 -0800
Subject: [PATCH] Yakir!

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe_mbi.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index db08bdab9..9bc92cb49 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -311,7 +311,7 @@ namespace qe {
         //for (app* a : avars) shared.push_back(a->get_decl());
         tg.set_vars(shared, false);
         tg.add_lits(lits);
-        //lits.reset();
+        lits.reset();
         lits.append(tg.project(*mdl.get()));
         TRACE("qe", tout << "project: " << lits << "\n";);                
     }
@@ -398,7 +398,9 @@ namespace qe {
         // sort avars based on depth
         struct compare_depth {
             bool operator()(app* x, app* y) const {
-                return x->get_depth() > y->get_depth();
+                return 
+                    (x->get_depth() > y->get_depth()) || 
+                    (x->get_depth() == y->get_depth() && x->get_id() > y->get_id());
             }
         };
         compare_depth cmpd;