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)) {