From b1bc890992e9f601109cf3e9c27a57fdcfac0213 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 28 Aug 2021 18:05:51 -0700
Subject: [PATCH] fix #5515

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_opt.cpp     |  1 +
 src/opt/opt_context.cpp |  1 +
 src/opt/opt_context.h   | 20 ++++++++++++++++++++
 3 files changed, 22 insertions(+)

diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index c0314ae79..a682a83da 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -325,6 +325,7 @@ extern "C" {
         RESET_ERROR_CODE();
         Z3_stats_ref * st = alloc(Z3_stats_ref, *mk_c(c));
         to_optimize_ptr(d)->collect_statistics(st->m_stats);
+        to_optimize_ptr(d)->collect_timer_stats(st->m_stats);
         mk_c(c)->save_object(st);
         Z3_stats r = of_stats(st);
         RETURN_Z3(r);
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 776502541..219b5488d 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -266,6 +266,7 @@ namespace opt {
     }
 
     lbool context::optimize(expr_ref_vector const& _asms) {
+        scoped_time _st(*this);
         if (m_pareto) {
             return execute_pareto();
         }
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 0ed7bf9f2..43f776a68 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -117,6 +117,17 @@ namespace opt {
             {}
         };
 
+      double m_time = 0;      
+      class scoped_time {
+        context& c;
+        timer t;
+      public:
+        scoped_time(context& c):c(c) { c.m_time = 0; }
+        ~scoped_time() { c.m_time = t.get_seconds(); }
+      };
+
+
+
         class scoped_state {
             ast_manager& m;
             arith_util   m_arith;
@@ -261,6 +272,13 @@ namespace opt {
             m_on_model_eh  = on_model; 
         }
 
+      
+        void collect_timer_stats(statistics& st) const {
+	  if (m_time != 0) 
+	    st.update("time", m_time);
+	}
+
+
     private:
         lbool execute(objective const& obj, bool committed, bool scoped);
         lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);        
@@ -340,6 +358,8 @@ namespace opt {
         // quantifiers
         bool is_qsat_opt();
         lbool run_qsat_opt();
+
+      
     };
 
 }