mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-17 23:21:28 +00:00
Code Activity

fix bug in rewriter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-11-22 14:56:41 -08:00
parent 5025c3c8a9
commit 0bf9369414
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/arith_rewriter.cpp
View file

@ -830,7 +830,7 @@ br_status arith_rewriter::mk_ite_core(expr* c, expr* t, expr* e, expr_ref & resu
if (v1 > v2) 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))); 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 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; return BR_DONE;
} }
expr* x, *y; expr* x, *y;