From f9dde2e8a4709ba37341dc12a9b4a3d543769668 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 Oct 2021 12:21:54 -0400
Subject: [PATCH] #5605

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxlex.cpp            | 9 +++++----
 src/opt/opt_context.cpp       | 3 ++-
 src/sat/smt/euf_relevancy.cpp | 4 ++++
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp
index a545aa92e53..46c7104d5e5 100644
--- a/src/opt/maxlex.cpp
+++ b/src/opt/maxlex.cpp
@@ -135,8 +135,10 @@ namespace opt {
             if (mdl) {
                 TRACE("opt", tout << *mdl << "\n";);
                 for (auto & soft : m_soft) {
-                    if (!mdl->is_true(soft.s)) 
-                        break;
+                    if (!mdl->is_true(soft.s)) {
+                        update_bounds();
+                        return;
+                    }
                     soft.set_value(l_true);
                     assert_value(soft);
                 }
@@ -151,9 +153,8 @@ namespace opt {
             unsigned sz = m_soft.size();
             for (unsigned i = 0; i < sz; ++i) {
                 auto& soft = m_soft[i];
-                if (soft.value != l_undef) {
+                if (soft.value != l_undef) 
                     continue;
-                }
                 expr_ref_vector asms(m);
                 asms.push_back(soft.s);
                 lbool is_sat = s().check_sat(asms);
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 219b5488d45..e78da961b62 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -24,6 +24,7 @@ Module Name:
 #include "ast/pb_decl_plugin.h"
 #include "ast/ast_smt_pp.h"
 #include "ast/ast_pp_util.h"
+#include "ast/ast_ll_pp.h"
 #include "ast/display_dimacs.h"
 #include "model/model_smt2_pp.h"
 #include "tactic/goal.h"
@@ -1200,7 +1201,7 @@ namespace opt {
 
     app* context::purify(generic_model_converter_ref& fm, expr* term) {
        std::ostringstream out;
-       out << mk_pp(term, m);
+       out << mk_bounded_pp(term, m, 3);
        app* q = m.mk_fresh_const(out.str(), term->get_sort());
        if (!fm) fm = alloc(generic_model_converter, m, "opt");
        if (m_arith.is_int_real(term)) {
diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index d7f7b901295..06c0469ea24 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -27,6 +27,7 @@ namespace euf {
             return;
         for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes) 
             m_auto_relevant_lim.push_back(m_auto_relevant.size());
+        std::cout << "add-auto " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
         m_auto_relevant.push_back(e);
     }
     
@@ -109,6 +110,9 @@ namespace euf {
             if (e)
                 todo.push_back(e);
         }
+        std::cout << "init-relevant\n";
+        for (expr* e : m_auto_relevant)
+            std::cout << "auto-relevant " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
         todo.append(m_auto_relevant);
         for (unsigned i = 0; i < todo.size(); ++i) {
             expr* e = todo[i];