mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix handling of global parameters, exceptions when optimization call gets cancelled

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-21 17:04:10 -08:00
parent 122a12c980
commit 77aac8d96f
3 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/api_context.h
View file

@ -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; }