From 69f9640fdff33d196be69dc9e03e996b25e21389 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Nov 2023 13:14:44 -0800
Subject: [PATCH] fix #7018

---
 src/opt/opt_context.cpp | 18 ++++++++++++------
 src/opt/opt_context.h   |  1 +
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 11eddc2eb..1b57a7200 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -213,7 +213,7 @@ namespace opt {
 
     void context::add_hard_constraint(expr* f, expr* t) {
         if (m_calling_on_model) 
-            throw default_exception("adding soft constraints is not supported during callbacks");
+            throw default_exception("adding hard constraints is not supported during callbacks");
         m_scoped_state.m_asms.push_back(t);
         m_scoped_state.add(m.mk_implies(t, f));
         clear_state();
@@ -905,12 +905,14 @@ namespace opt {
             ptr_vector<expr> deps;
             expr_dependency_ref core(r->dep(i), m);
             m.linearize(core, deps);
-            if (!deps.empty()) {
-                fmls.push_back(m.mk_implies(m.mk_and(deps.size(), deps.data()), r->form(i)));
-            }
-            else {
+            if (deps.empty())
+                fmls.push_back(r->form(i));                
+            else if (deps.size() == 1 && deps[0] == r->form(i))
+                continue;
+            else if (is_objective(r->form(i)))
                 fmls.push_back(r->form(i));
-            }
+            else
+                fmls.push_back(m.mk_implies(mk_and(m, deps.size(), deps.data()), r->form(i)));
         }        
         if (r->inconsistent()) {
             ptr_vector<expr> core_elems;
@@ -920,6 +922,10 @@ namespace opt {
         }
     }
 
+    bool context::is_objective(expr* fml) {
+        return is_app(fml) && m_objective_fns.contains(to_app(fml)->get_decl());
+    }
+
     bool context::is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) {
         if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) && 
             m_objectives[index].m_type == O_MAXIMIZE) {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 9e61ae92c..4e791531e 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -303,6 +303,7 @@ namespace opt {
         void import_scoped_state();
         void normalize(expr_ref_vector const& asms);
         void internalize();
+        bool is_objective(expr* fml);
         bool is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
         bool is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
         bool is_maxsat(expr* fml, expr_ref_vector& terms,