From 2da7a8dd704b0e2d334ed686ea59a2ef4a48a0bf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2020 20:12:11 -0700 Subject: [PATCH] fix #4491 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 471cb7643..77ded074b 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -345,7 +345,7 @@ br_status arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, exp continue; eqs.push_back(m().mk_eq(arg, zero)); } - result = m().mk_and(eqs); + result = m().mk_or(eqs); return BR_REWRITE2; }