mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

Fix for timeout/rlimit in deprecated solver API.

Browse source 
Partially fixes #307.
This commit is contained in:
Christoph M. Wintersteiger 2015-11-13 16:42:46 +00:00
parent 954400cfa2
commit 15c48eeaf9
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/api_solver_old.cpp
View file

@ -23,6 +23,8 @@ Revision History:
#include"api_context.h" #include"api_context.h"
#include"api_model.h" #include"api_model.h"
#include"cancel_eh.h" #include"cancel_eh.h"
#include"scoped_timer.h"
#include"rlimit.h"
extern "C" { extern "C" {
@ -75,8 +77,13 @@ extern "C" {
cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel()); cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
api::context::set_interruptable si(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
flet<bool> _model(mk_c(c)->fparams().m_model, true); flet<bool> _model(mk_c(c)->fparams().m_model, true);
unsigned timeout = mk_c(c)->params().m_timeout;
unsigned rlimit = mk_c(c)->params().m_rlimit;
lbool result; lbool result;
try { try {
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
model_ref _m; model_ref _m;
result = mk_c(c)->check(_m); result = mk_c(c)->check(_m);
if (m) { if (m) {