From 0bf9369414ec577a8eb2e4345ae99e1c7e618178 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 Nov 2024 14:56:41 -0800 Subject: [PATCH] fix bug in rewriter Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 93949f4db..e868a6eb2 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -830,7 +830,7 @@ br_status arith_rewriter::mk_ite_core(expr* c, expr* t, expr* e, expr_ref & resu if (v1 > v2) result = m_util.mk_add(e, m.mk_ite(c, m_util.mk_numeral(v1 - v2, is_int), m_util.mk_numeral(rational::zero(), is_int))); else - result = m_util.mk_add(e, m.mk_ite(c, m_util.mk_numeral(rational::zero(), is_int), m_util.mk_numeral(v2 - v1, is_int))); + result = m_util.mk_add(t, m.mk_ite(c, m_util.mk_numeral(rational::zero(), is_int), m_util.mk_numeral(v2 - v1, is_int))); return BR_DONE; } expr* x, *y;