From 709a5d9524a8e04280b034b4d9681aa91dde36a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Mar 2016 16:09:12 -0700 Subject: [PATCH] fix bug: & -> && Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- src/ast/simplifier/arith_simplifier_plugin.cpp | 3 ++- src/ast/simplifier/simplifier.cpp | 1 + 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 24d69cc0e..c9a2d2379 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -695,7 +695,7 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu result = m_util.mk_numeral(div(v1, v2), is_int); return BR_DONE; } - if (m_util.is_numeral(arg2, v2, is_int) & v2.is_zero()) { + if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) { result = m_util.mk_idiv0(arg1); return BR_REWRITE1; } diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp index f7751782d..588508f4f 100644 --- a/src/ast/simplifier/arith_simplifier_plugin.cpp +++ b/src/ast/simplifier/arith_simplifier_plugin.cpp @@ -406,8 +406,9 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co case OP_POWER: return false; case OP_ABS: SASSERT(num_args == 1); mk_abs(args[0], result); break; case OP_IRRATIONAL_ALGEBRAIC_NUM: return false; + case OP_DIV_0: return false; + case OP_IDIV_0: return false; default: - UNREACHABLE(); return false; } TRACE("arith_simplifier_plugin", tout << mk_pp(result.get(), m_manager) << "\n";); diff --git a/src/ast/simplifier/simplifier.cpp b/src/ast/simplifier/simplifier.cpp index 2a152283f..895aa529b 100644 --- a/src/ast/simplifier/simplifier.cpp +++ b/src/ast/simplifier/simplifier.cpp @@ -473,6 +473,7 @@ void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args //dump_rewrite_lemma(decl, num_args, args, result.get()); return; } + result = m.mk_app(decl, num_args, args); }