From 5307797c3251843ce2c91a0769afda166825ae57 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 May 2020 21:03:27 -0700 Subject: [PATCH] #4424 --- src/cmd_context/context_params.cpp | 7 ++++--- src/smt/smt_context.cpp | 2 +- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index fd5892217..6289d33c5 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -119,7 +119,8 @@ void context_params::set(char const * param, char const * value) { m_dot_proof_file = value; } else if (p == "unsat_core") { - set_bool(m_unsat_core, param, value); + if (!m_unsat_core) + set_bool(m_unsat_core, param, value); } else if (p == "debug_ref_count") { set_bool(m_debug_ref_count, param, value); @@ -154,7 +155,7 @@ void context_params::updt_params(params_ref const & p) { m_trace = p.get_bool("trace", m_trace); m_trace_file_name = p.get_str("trace_file_name", "z3.log"); m_dot_proof_file = p.get_str("dot_proof_file", "proof.dot"); - m_unsat_core = p.get_bool("unsat_core", m_unsat_core); + 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); m_statistics = p.get_bool("stats", m_statistics); @@ -198,7 +199,7 @@ params_ref context_params::merge_default_params(params_ref const & p) { void context_params::get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) { proofs_enabled = m.proofs_enabled() && p.get_bool("proof", m_proof); models_enabled = p.get_bool("model", m_model); - unsat_core_enabled = p.get_bool("unsat_core", m_unsat_core); + unsat_core_enabled = m_unsat_core || p.get_bool("unsat_core", false); p = merge_default_params(p); } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 709dabd09..b732b792d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1601,7 +1601,7 @@ namespace smt { if (inconsistent()) return false; } -#if 0 +#if 1 if (at_search_level() && induction::should_try(*this)) { get_induction()(); }