From 044d6316ca7435ba9b4e107ada8be25a72db2abc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 19 Mar 2020 09:39:21 -0700
Subject: [PATCH] fix #3417

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_solver.cpp | 1 -
 src/opt/optsmt.cpp     | 2 --
 2 files changed, 3 deletions(-)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index de88b9257..503cd8366 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -434,7 +434,6 @@ namespace opt {
             return th.mk_ge(m_fm, v, val);
         }
 
-
         if (typeid(smt::theory_lra) == typeid(opt)) {
             smt::theory_lra& th = dynamic_cast<smt::theory_lra&>(opt); 
             SASSERT(val.is_finite());
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index dfb5e7061..723ee17cf 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -372,9 +372,7 @@ namespace opt {
                        else
                            verbose_stream() << "(optsmt upper bound: " << (-v) << ")\n";
                        );            
-            expr_ref tmp(m);
             for (unsigned i = idx+1; i < m_vars.size(); ++i) {
-                m_s->maximize_objective(i, tmp);
                 m_lower[i] = m_s->saved_objective_value(i);
             }
             m_best_model = m_model;