1

Closed

Z3_interrupt ignored

description

Since upgrading to the open source version of Z3, we've had problems with our (KLEE) tool not being able to trigger solver timeouts from a watchdog thread using Z3_interrupt (or Z3_soft_check_cancel).

After a little debugging, I tracked it down to the set_interruptable class. The ctor sets the context m_interruptable field, and the dtor resets it. Unfortunately, the dtor is immediately called in all the places where set_interruptable is used. This doesn't seem to be the intended behavior. The patch below should address the issue.

-David
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index aeddf63..463cb03 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -679,7 +679,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 394df7a..65f0344 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -312,7 +312,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", UINT_MAX);
-        api::context::set_interruptable(*(mk_c(c)), eh);        
+        api::context::set_interruptable si(*(mk_c(c)), eh);        
         {
             scoped_timer timer(timeout, &eh);
             try {
@@ -337,7 +337,7 @@ extern "C" {
         lbool r = l_undef;
         unsigned timeout = to_fixedpoint(d)->m_params.get_uint(":timeout", UINT_MAX);
         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_solver.cpp b/src/api/api_solver.cpp
index 790ca8f..45c2f5c 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -241,7 +241,7 @@ extern "C" {
         unsigned timeout     = to_solver(s)->m_params.get_uint(":timeout", UINT_MAX);
         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 cd4b797..5a611c6 100644
--- a/src/api/api_solver_old.cpp
+++ b/src/api/api_solver_old.cpp
@@ -74,7 +74,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 {
@@ -137,7 +137,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 ff55923..34de75d 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);

file attachments

Closed Mar 25, 2013 at 11:54 PM by leodemoura
Issue was fixed in the unstable branch.

comments

leodemoura wrote Mar 25, 2013 at 11:53 PM

Thanks for catching this problem. I fixed the problem in the unstable (working-in-progress) branch. The fix will be available in the next official release. In the meantime, consider using the unstable branch. The fix will also be available tomorrow in the nightly builds.