From 752a6b2e33c954eba65a2d88d3b8e6ef82a251e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Jul 2014 16:46:27 +0200 Subject: [PATCH] fix quantifier elimination bugs reported by Berdine and Bornat Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index e67300970..b040efc0c 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -704,7 +704,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul } // propagate mod inside only if not all arguments are not already mod. - if (false && m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { + if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";); unsigned num_args = to_app(arg1)->get_num_args(); unsigned i;