mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Set :print-success to true, when SMTLIB2_COMPLIANT mode is set.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-02-02 08:58:59 -08:00
parent ca74b2d6cf
commit 8480b27311
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/cmd_context/cmd_context.cpp
View file

@ -304,8 +304,8 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_main_ctx(main_ctx),
m_logic(l),
m_interactive_mode(false),
m_global_decls(false), // :global-decls is false by default.
m_print_success(false), // params.m_smtlib2_compliant),
m_global_decls(false),
m_print_success(m_params.m_smtlib2_compliant),
m_random_seed(0),
m_produce_unsat_cores(false),
m_produce_assignments(false),
@ -352,6 +352,8 @@ void cmd_context::set_cancel(bool f) {
void cmd_context::global_params_updated() {
m_params.updt_params();
if (m_params.m_smtlib2_compliant)
m_print_success = true;
if (m_solver) {
params_ref p;
if (!m_params.m_auto_config)