From 755a259ea0fac2d8568b3f277add7f169fb9bd44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Mar 2015 00:44:56 -0700 Subject: [PATCH] fix codeplex issue 188 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/context_params.cpp | 30 ++++++++++++++++++++---------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index f87c8d264..13f6f5be3 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -24,6 +24,16 @@ Notes: #include"solver.h" context_params::context_params() { + m_unsat_core = false; + m_model = true; + m_model_validate = false; + m_auto_config = true; + m_proof = false; + m_trace = false; + m_debug_ref_count = false; + m_smtlib2_compliant = false; + m_well_sorted_check = false; + m_timeout = UINT_MAX; updt_params(); } @@ -98,17 +108,17 @@ void context_params::updt_params() { } void context_params::updt_params(params_ref const & p) { - m_timeout = p.get_uint("timeout", UINT_MAX); - m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true)); - m_auto_config = p.get_bool("auto_config", true); - m_proof = p.get_bool("proof", false); - m_model = p.get_bool("model", true); - m_model_validate = p.get_bool("model_validate", false); - m_trace = p.get_bool("trace", false); + m_timeout = p.get_uint("timeout", m_timeout); + m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", m_well_sorted_check)); + m_auto_config = p.get_bool("auto_config", m_auto_config); + m_proof = p.get_bool("proof", m_proof); + m_model = p.get_bool("model", m_model); + m_model_validate = p.get_bool("model_validate", m_model_validate); + m_trace = p.get_bool("trace", m_trace); m_trace_file_name = p.get_str("trace_file_name", "z3.log"); - m_unsat_core = p.get_bool("unsat_core", false); - m_debug_ref_count = p.get_bool("debug_ref_count", false); - m_smtlib2_compliant = p.get_bool("smtlib2_compliant", false); + m_unsat_core = p.get_bool("unsat_core", m_unsat_core); + m_debug_ref_count = p.get_bool("debug_ref_count", m_debug_ref_count); + m_smtlib2_compliant = p.get_bool("smtlib2_compliant", m_smtlib2_compliant); } void context_params::collect_param_descrs(param_descrs & d) {