From c7af97364a55394396b69feb04c449aa3fe60f1f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 1 Oct 2024 15:15:47 -0700
Subject: [PATCH] fixes for #7402

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 31 ++++++++++++++++---------------
 1 file changed, 16 insertions(+), 15 deletions(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index c571753e9..f3b4c78b7 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -401,9 +401,24 @@ namespace opt {
     void context::set_model(model_ref& m) { 
         m_model = m;
         opt_params optp(m_params);
-        if (optp.dump_models() && m) {
+        symbol prefix = optp.solution_prefix();
+        bool model2console = optp.dump_models();
+        bool model2file = prefix != symbol::null && prefix != symbol("");
+    
+        if ((model2console || model2file) && m) {
             model_ref md = m->copy();
             fix_model(md);
+            if (model2file) {
+                std::ostringstream buffer;
+                buffer << prefix << (m_model_counter++) << ".smt2";
+                std::ofstream out(buffer.str());        
+                if (out) {
+                    out << *md;
+                    out.close();
+                }
+            }
+            if (model2console)
+                std::cout << *md;
         }
         if (m_on_model_eh && m) {
             model_ref md = m->copy();
@@ -1168,20 +1183,6 @@ namespace opt {
     void context::model_updated(model* md) {
         model_ref mdl = md;
         set_model(mdl);
-#if 0
-        opt_params optp(m_params);
-        symbol prefix = optp.solution_prefix();
-        if (prefix == symbol::null || prefix == symbol("")) return;        
-        model_ref mdl = md->copy();
-        fix_model(mdl);
-        std::ostringstream buffer;
-        buffer << prefix << (m_model_counter++) << ".smt2";
-        std::ofstream out(buffer.str());        
-        if (out) {
-            out << *mdl;
-            out.close();
-        }
-#endif
     }
 
     rational context::adjust(unsigned id, rational const& v) {