From 557cda70b0ce9c05d5ba2a4ed0221d36a44c5b2d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Nov 2012 08:45:31 -0800 Subject: [PATCH] Set :global-decls to false Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 3 +++ src/cmd_context/cmd_context.cpp | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 2bf6fb7b0..845b11395 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -7,6 +7,9 @@ Version 4.3.2 - Added support for FreeBSD. Z3 can be compiled on FreeBSD using g++. +- Reverted to `(set-option :global-decls false)` as the default. In Z3 4.3.0 and Z3 4.3.1, this option was set to false. + Thanks to Julien Henry for reporting this problem. + Version 4.3.1 ============= diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 225f0be87..0fb4b8512 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -306,7 +306,7 @@ cmd_context::cmd_context(front_end_params * params, bool main_ctx, ast_manager * m_params_owner(params == 0), m_logic(l), m_interactive_mode(false), - m_global_decls(!this->params().m_smtlib2_compliant), // SMTLIB 2.0 uses scoped decls. + m_global_decls(false), // :global-decls is false by default. m_print_success(false), // params.m_smtlib2_compliant), m_random_seed(0), m_produce_unsat_cores(false),