From 6d79b191703ea9b85fbb1304ee97fd5b7832b4ab Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 11 Jun 2018 22:08:50 -0700
Subject: [PATCH] fix a few bugs, debugging eufi

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe_mbi.cpp        |  2 +-
 src/qe/qe_term_graph.cpp | 28 ++++++++++++++++++++--------
 src/solver/mus.cpp       |  4 ++--
 3 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index 4b86a10a4..298a1da99 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -116,7 +116,7 @@ namespace qe {
         m_dual_solver(sNot)
     {
         params_ref p;
-        p.set_bool("smt.core.minimize", true);
+        p.set_bool("core.minimize", true);
         m_solver->updt_params(p);
         m_dual_solver->updt_params(p);
         expr_ref_vector fmls(m);
diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index 8e3981e64..f537c5da8 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -625,7 +625,7 @@ namespace qe {
 
             expr_ref_vector m_pinned;  // tracks expr in the maps
 
-            expr* mk_pure(term& t) {
+            expr* mk_pure(term const& t) {
         expr* e = nullptr;
         if (m_term2app.find(t.get_id(), e)) return e;
         e = t.get_expr();
@@ -643,7 +643,7 @@ namespace qe {
     }
 
             bool is_better_rep(expr *t1, expr *t2) {
-                if (!t2) return t1;
+                if (!t2) return t1 != nullptr;
                 return m.is_unique_value(t1) && !m.is_unique_value(t2);
             }
 
@@ -755,13 +755,21 @@ namespace qe {
     }
 
             void mk_pure_equalities(const term &t, expr_ref_vector &res) {
+                SASSERT(t.is_root());
                 expr *rep = nullptr;
                 if (!m_root2rep.find(t.get_id(), rep)) return;
-                for (term *it = &t.get_next(); it != &t; it = &it->get_next()) {
-                    expr* member = mk_pure(*it);
-                    if (member)
+                obj_hashtable<expr> members;
+                members.insert(rep);
+                term const * r = &t;
+                do {
+                    expr* member = nullptr;
+                    if (m_term2app.find(r->get_id(), member) && !members.contains(member)) {
                         res.push_back (m.mk_eq (rep, member));
+                        members.insert(member);
+                    }
+                    r = &r->get_next();
                 }
+                while (r != &t);
             }
 
             bool is_projected(const term &t) {
@@ -771,13 +779,17 @@ namespace qe {
             void mk_unpure_equalities(const term &t, expr_ref_vector &res) {
                 expr *rep = nullptr;
                 if (!m_root2rep.find(t.get_id(), rep)) return;
-                for (term *it = &t.get_next(); it != &t; it = &it->get_next()) {
-                    expr* member = mk_pure(*it);
+                obj_hashtable<expr> members;
+                term const * r = &t;
+                do {
+                    expr* member = mk_pure(*r);
                     SASSERT(member);
-                    if (!is_projected(*it) || !is_solved_eq(rep, member)) {
+                    if (member != rep && (!is_projected(*r) || !is_solved_eq(rep, member))) {
                         res.push_back(m.mk_eq(rep, member));
                     }
+                    r = &r->get_next();
                 }
+                while (r != &t);
             }
 
             void mk_equalities(bool pure, expr_ref_vector &res) {
diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp
index e4ebd7e3b..a7925f268 100644
--- a/src/solver/mus.cpp
+++ b/src/solver/mus.cpp
@@ -50,12 +50,12 @@ struct mus::imp {
     }
 
     bool is_literal(expr* lit) const {
-        expr* l;
+        expr* l;		
         return is_uninterp_const(lit) || (m.is_not(lit, l) && is_uninterp_const(l));
     }
     
     unsigned add_soft(expr* lit) {
-        SASSERT(is_literal(lit));
+        //SASSERT(is_literal(lit));
         unsigned idx = m_lit2expr.size();
         m_expr2lit.insert(lit, idx);
         m_lit2expr.push_back(lit);