From b417ca657d388a3f635b19f371b5d3975835f412 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Mar 2013 16:52:08 -0700
Subject: [PATCH] Fix set_interruptable usage

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/api/api_algebraic.cpp  | 4 ++--
 src/api/api_ast.cpp        | 2 +-
 src/api/api_datalog.cpp    | 4 ++--
 src/api/api_polynomial.cpp | 2 +-
 src/api/api_solver.cpp     | 2 +-
 src/api/api_solver_old.cpp | 4 ++--
 src/api/api_tactic.cpp     | 2 +-
 7 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp
index 7716cbb59..d03a6aff4 100644
--- a/src/api/api_algebraic.cpp
+++ b/src/api/api_algebraic.cpp
@@ -373,7 +373,7 @@ extern "C" {
         scoped_anum_vector roots(_am);
         {
             cancel_eh<algebraic_numbers::manager> eh(_am);
-            api::context::set_interruptable(*(mk_c(c)), eh);
+            api::context::set_interruptable si(*(mk_c(c)), eh);
             scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
             vector_var2anum v2a(as);
             _am.isolate_roots(_p, v2a, roots);
@@ -408,7 +408,7 @@ extern "C" {
         }
         {
             cancel_eh<algebraic_numbers::manager> eh(_am);
-            api::context::set_interruptable(*(mk_c(c)), eh);
+            api::context::set_interruptable si(*(mk_c(c)), eh);
             scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
             vector_var2anum v2a(as);
             int r = _am.eval_sign_at(_p, v2a);
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index e93e1a178..680b59c68 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -681,7 +681,7 @@ extern "C" {
         th_rewriter m_rw(m, p);
         expr_ref    result(m);
         cancel_eh<th_rewriter> eh(m_rw);
-        api::context::set_interruptable(*(mk_c(c)), eh);
+        api::context::set_interruptable si(*(mk_c(c)), eh);
         {
             scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 28fe3ed33..0f100e747 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -266,7 +266,7 @@ extern "C" {
         lbool r = l_undef;
         cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
         unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
-        api::context::set_interruptable(*(mk_c(c)), eh);        
+        api::context::set_interruptable si(*(mk_c(c)), eh);        
         {
             scoped_timer timer(timeout, &eh);
             try {
@@ -291,7 +291,7 @@ extern "C" {
         lbool r = l_undef;
         unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
         cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
-        api::context::set_interruptable(*(mk_c(c)), eh);
+        api::context::set_interruptable si(*(mk_c(c)), eh);
         {
             scoped_timer timer(timeout, &eh);
             try {
diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp
index 3148f972b..25d4ca292 100644
--- a/src/api/api_polynomial.cpp
+++ b/src/api/api_polynomial.cpp
@@ -67,7 +67,7 @@ extern "C" {
             expr_ref _r(mk_c(c)->m());
             {
                 cancel_eh<polynomial::manager> eh(pm);
-                api::context::set_interruptable(*(mk_c(c)), eh);
+                api::context::set_interruptable si(*(mk_c(c)), eh);
                 scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
                 pm.psc_chain(_p, _q, v_x, rs);
             }
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 9ace149af..ac30a0c21 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -243,7 +243,7 @@ extern "C" {
         unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
         bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);
         cancel_eh<solver> eh(*to_solver_ref(s));
-        api::context::set_interruptable(*(mk_c(c)), eh);
+        api::context::set_interruptable si(*(mk_c(c)), eh);
         lbool result;
         {
             scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp
index c89f89873..e0533fbd9 100644
--- a/src/api/api_solver_old.cpp
+++ b/src/api/api_solver_old.cpp
@@ -73,7 +73,7 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_SEARCHING(c);
         cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
-        api::context::set_interruptable(*(mk_c(c)), eh);
+        api::context::set_interruptable si(*(mk_c(c)), eh);
         flet<bool> _model(mk_c(c)->fparams().m_model, true);
         lbool result;
         try {
@@ -123,7 +123,7 @@ extern "C" {
         expr * const* _assumptions = to_exprs(assumptions);
         flet<bool> _model(mk_c(c)->fparams().m_model, true);
         cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
-        api::context::set_interruptable(*(mk_c(c)), eh);
+        api::context::set_interruptable si(*(mk_c(c)), eh);
         lbool result;
         result = mk_c(c)->get_smt_kernel().check(num_assumptions, _assumptions);
         if (result != l_false && m) {
diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index 5bce218e6..911360047 100644
--- a/src/api/api_tactic.cpp
+++ b/src/api/api_tactic.cpp
@@ -410,7 +410,7 @@ extern "C" {
         
         to_tactic_ref(t)->updt_params(p);
 
-        api::context::set_interruptable(*(mk_c(c)), eh);
+        api::context::set_interruptable si(*(mk_c(c)), eh);
         {
             scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
             scoped_timer timer(timeout, &eh);