From 16413b4f9aec688af52aed6152175f6b76b6e37f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Jul 2021 17:18:22 -0700
Subject: [PATCH] #5429

---
 src/math/simplex/model_based_opt.cpp |  3 ++-
 src/sat/smt/q_clause.cpp             | 18 +++++++++---------
 src/sat/smt/q_mbi.cpp                |  1 -
 3 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 1acbb592b..83e83cfe7 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -1261,7 +1261,8 @@ namespace opt {
             m_var2value[x] = eval(result);
             TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);
         }
-        retire_row(row_id1);
+        else 
+            retire_row(row_id1);
         return result;
     }
     
diff --git a/src/sat/smt/q_clause.cpp b/src/sat/smt/q_clause.cpp
index 7c8a260e5..097a61a14 100644
--- a/src/sat/smt/q_clause.cpp
+++ b/src/sat/smt/q_clause.cpp
@@ -23,9 +23,9 @@ namespace q {
     std::ostream& lit::display(std::ostream& out) const {
         ast_manager& m = lhs.m();
         if (m.is_true(rhs) && !sign) 
-            return out << mk_bounded_pp(lhs, m, 2);
+            return out << lhs;
         if (m.is_false(rhs) && !sign) 
-            return out << "(not " << mk_bounded_pp(lhs, m, 2) << ")";
+            return out << "(not " << lhs << ")";
         return 
             out << mk_bounded_pp(lhs, m, 2) 
                 << (sign ? " != " : " == ") 
@@ -43,13 +43,13 @@ namespace q {
         for (auto const& lit : m_lits)
             lit.display(out) << "\n";
         binding* b = m_bindings;
-        if (b) {
-            do {
-                b->display(ctx, num_decls(), out) << "\n";
-                b = b->next();
-            }
-            while (b != m_bindings);
-        }
+        if (!b)
+            return out;
+        do {
+            b->display(ctx, num_decls(), out) << "\n";
+            b = b->next();
+        } 
+        while (b != m_bindings);
         return out;
     }
 
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index 5c30bedd4..03d748236 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -162,7 +162,6 @@ namespace q {
                 return r;
             if (r == l_true) {
                 model_ref mdl;
-                expr_ref proj(m);
                 m_solver->get_model(mdl);
                 if (check_forall_subst(q, *qb, *mdl))
                     return l_false;