From 87d556d37d6dfa9319f1a4f2cb329aabb6d14495 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 24 Aug 2024 10:57:35 -0700 Subject: [PATCH] delay factoring Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 0919c973a..b67e873c0 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -651,11 +651,6 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin arg1 = new_arg1; arg2 = new_arg2; } - { - br_status st1 = factor_le_ge_eq(arg1, arg2, kind, result); - if (st1 != BR_FAILED) - return st1; - } expr_ref new_new_arg1(m); expr_ref new_new_arg2(m); if (m_elim_to_real && elim_to_real(arg1, arg2, new_new_arg1, new_new_arg2)) { @@ -783,7 +778,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin default: result = m.mk_eq(arg1, arg2); return BR_DONE; } } - return BR_FAILED; + return factor_le_ge_eq(arg1, arg2, kind, result); }