From 77aac8d96fc115fef9cbf4c3cdd007a190df41ba Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Feb 2017 17:04:10 -0800
Subject: [PATCH] fix handling of global parameters, exceptions when
 optimization call gets cancelled

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_context.h       | 6 +++---
 src/api/api_opt.cpp         | 8 +++++++-
 src/sat/tactic/goal2sat.cpp | 1 -
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/api/api_context.h b/src/api/api_context.h
index 4685fd04e..d26cb0b1e 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -113,13 +113,13 @@ namespace api {
         ~context();
         ast_manager & m() const { return *(m_manager.get()); }
 
-        context_params & params() { return m_params; }
+        context_params & params() { m_params.updt_params(); return m_params; }
         bool produce_proofs() const { return m().proofs_enabled(); }
         bool produce_models() const { return m_params.m_model; }
         bool produce_unsat_cores() const { return m_params.m_unsat_core; }
         bool use_auto_config() const { return m_params.m_auto_config; }
-        unsigned get_timeout() const { return m_params.m_timeout; }
-        unsigned get_rlimit() const { return m_params.m_rlimit; }
+        unsigned get_timeout() { return params().m_timeout; }
+        unsigned get_rlimit() { return params().m_rlimit; }
         arith_util & autil() { return m_arith_util; }
         bv_util & bvutil() { return m_bv_util; }
         datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index 3d8580178..6fbc86ab6 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -129,6 +129,7 @@ extern "C" {
         cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout());
         unsigned rlimit = mk_c(c)->get_rlimit();
+        std::cout << "Timeout: " << timeout << "\n";
         api::context::set_interruptable si(*(mk_c(c)), eh);        
         {
             scoped_timer timer(timeout, &eh);
@@ -137,8 +138,13 @@ extern "C" {
                 r = to_optimize_ptr(o)->optimize();
             }
             catch (z3_exception& ex) {
-                mk_c(c)->handle_exception(ex);
                 r = l_undef;
+                if (ex.msg() == "canceled" && mk_c(c)->m().canceled()) {
+                    to_optimize_ptr(o)->set_reason_unknown(ex.msg());
+                }
+                else {
+                    mk_c(c)->handle_exception(ex);
+                }
             }
             // to_optimize_ref(d).cleanup();
         }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 93367013e..30a458ece 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -85,7 +85,6 @@ struct goal2sat::imp {
         m_ite_extra       = p.get_bool("ite_extra", true);
         m_max_memory      = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
         m_cardinality_solver = p.get_bool("cardinality_solver", false);
-        std::cout << p << "\n";
     }
 
     void throw_op_not_handled(std::string const& s) {