From b758a7a508775ad0a848ab54349c13c2f9f8c2dc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Sep 2016 19:53:48 -0700 Subject: [PATCH] disable smt-lib success printing when locally parsing database of common pattern rules. Issue #743 Signed-off-by: Nikolaj Bjorner --- src/ast/pattern/expr_pattern_match.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp index 86cad58f8..e18831650 100644 --- a/src/ast/pattern/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -388,7 +388,10 @@ expr_pattern_match::initialize(char const * spec_string) { std::istringstream is(spec_string); cmd_context ctx(true, &m_manager); + bool ps = ctx.print_success_enabled(); + ctx.set_print_success(false); VERIFY(parse_smt2_commands(ctx, is)); + ctx.set_print_success(ps); ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions();