From 10894069b09c13c0ff7593cdd8eaa86c2009d5a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Feb 2018 13:19:40 -0800 Subject: [PATCH] fix compiler error reported by Luca Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 3b657f1a3..8125a651a 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -471,7 +471,8 @@ struct pb2bv_rewriter::imp { expr_ref gt = mod_ge(out, B, d_i + 1); expr_ref ge = mod_ge(out, B, d_i); - result = mk_or(gt, mk_and(ge, result)); + result = mk_and(ge, result); + result = mk_or(gt, result); TRACE("pb", tout << "b: " << b_i << " d: " << d_i << " gt: " << gt << " ge: " << ge << " " << result << "\n";); new_carry.reset();