From 202ed79a24479a4cc63596c145e87030e12c481f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Aug 2021 11:17:23 -0700
Subject: [PATCH] #5445

---
 src/math/simplex/model_based_opt.cpp | 2 ++
 src/sat/smt/euf_solver.cpp           | 9 +++------
 src/util/sexpr.cpp                   | 4 +++-
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 1acbb592b..6c0d48f96 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -1227,6 +1227,8 @@ namespace opt {
 
         if (m_var2is_int[x] && !a.is_one()) {
             row& r1 = m_rows[row_id1];
+            r1.m_coeff -= r1.m_value;
+            r1.m_value = 0;
             vector<var> coeffs;
             mk_coeffs_without(coeffs, r1.m_vars, x);
             rational c = mod(-eval(coeffs), a);
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index d2ae0a0dd..3e1620090 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -315,14 +315,11 @@ namespace euf {
             m_egraph.merge(n, nb, c);
         }
         if (n->is_equality()) {
+            SASSERT(!m.is_iff(e));
             if (sign)
                 m_egraph.new_diseq(n);
-            else {
-                SASSERT(!m.is_iff(e));
-                euf::enode* na = n->get_arg(0);
-                euf::enode* nb = n->get_arg(1);
-                m_egraph.merge(na, nb, c);
-            }
+            else                 
+                m_egraph.merge(n->get_arg(0), n->get_arg(1), c);            
         }    
     }
 
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index bebce4273..e20c56234 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -185,8 +185,10 @@ void sexpr::display_atom(std::ostream & out) const {
 }
 
 void sexpr::display(std::ostream & out) const {
-    if (!is_composite())
+    if (!is_composite()) {
         display_atom(out);
+        return;
+    }
     vector<std::pair<sexpr_composite const *, unsigned> > todo;
     todo.push_back(std::make_pair(static_cast<sexpr_composite const *>(this), 0));
     while (!todo.empty()) {