From ed70d246d37278259ec25c80ccbbf22319c4254a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Mar 2020 11:39:09 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/poly_rewriter_def.h | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index ac83972ac..de98f33fa 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -788,14 +788,8 @@ br_status poly_rewriter::cancel_monomials(expr * lhs, expr * rhs, bool m normalize(c); if (!has_multiple && num_coeffs <= 1) { -#if 0 - if (num_coeffs == 0 || is_numeral(rhs)) { - return BR_FAILED; - } -#else if (move) { if (is_numeral(rhs)) { - std::cout << mk_pp(lhs, m()) << " " << mk_pp(rhs, m()) << "\n"; return BR_FAILED; } } @@ -804,7 +798,6 @@ br_status poly_rewriter::cancel_monomials(expr * lhs, expr * rhs, bool m return BR_FAILED; } } -#endif } TRACE("le_bug", tout << num_coeffs << " " << mk_pp(lhs, m()) << " " << mk_pp(rhs, m()) << "\n";);