From 67d3f3b1102d604ce36703c303bdd114e90c629c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 24 Aug 2024 10:14:59 -0700 Subject: [PATCH] localize impact of factoring Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index a9a59bd6a..0919c973a 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -651,9 +651,11 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin arg1 = new_arg1; arg2 = new_arg2; } - st = factor_le_ge_eq(arg1, arg2, kind, result); - if (st != BR_FAILED) - return st; + { + 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)) {