From 05d9e188f856555389333bc89ed039924656933d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Sep 2015 14:08:04 +0100 Subject: [PATCH] Reactivated smt.max_conflicts option. Partially fixes #216. --- src/smt/params/smt_params.cpp | 1 + src/smt/params/smt_params_helper.pyg | 1 + 2 files changed, 2 insertions(+) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 6028bbb24..2ef9a0d54 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -35,6 +35,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_delay_units_threshold = p.delay_units_threshold(); m_preprocess = _p.get_bool("preprocess", true); // hidden parameter m_timeout = p.timeout(); + m_max_conflicts = p.max_conflicts(); m_core_validate = p.core_validate(); model_params mp(_p); m_model_compact = mp.compact(); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 5cd9cdcdc..fa73f9725 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -16,6 +16,7 @@ def_module_params(module_name='smt', ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), ('timeout', UINT, 0, 'timeout (0 means no timeout)'), + ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'), ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'), ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'), ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),