From 244cbc263831823096359f4745db259f6de5845b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Jun 2017 10:04:50 -0700 Subject: [PATCH] ensure that auxiliary PB booleans are recognized during rewriting. Fixes segementation fault #1113, but does not address performance issues with quantifiers and optimization combinations Signed-off-by: Nikolaj Bjorner --- src/ast/pb_decl_plugin.h | 1 + src/ast/rewriter/pb_rewriter.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index 0750dcac7..36b1a9512 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -109,6 +109,7 @@ public: bool is_ge(func_decl* a) const; bool is_ge(expr* a) const { return is_app(a) && is_ge(to_app(a)->get_decl()); } bool is_ge(expr* a, rational& k) const; + bool is_aux_bool(func_decl* f) const { return is_decl_of(f, m_fid, OP_PB_AUX_BOOL); } bool is_aux_bool(expr* e) const { return is_app_of(e, m_fid, OP_PB_AUX_BOOL); } rational get_coeff(expr* a, unsigned index) const { return get_coeff(to_app(a)->get_decl(), index); } rational get_coeff(func_decl* a, unsigned index) const; diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index 0fdbc858d..b14d350b1 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -196,6 +196,7 @@ void pb_rewriter::dump_pb_rewrite(expr* fml) { } br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { + if (m_util.is_aux_bool(f)) return BR_FAILED; ast_manager& m = result.get_manager(); rational sum(0), maxsum(0); for (unsigned i = 0; i < num_args; ++i) {