From 1d77e3e19f67c7fd07e5f89713bd079331c4090c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Dec 2019 14:41:09 -0800 Subject: [PATCH] fix #2830 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bool_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 39afbf1bb..eab1b79a6 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -752,7 +752,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args if (!m().is_unique_value(arg)) all_value = false; if (!all_value && all_diff) { - for (unsigned j = 0; all_diff && j + 1 < i; ++j) { + for (unsigned j = 0; all_diff && j < i; ++j) { all_diff = m().are_distinct(arg, args[j]); } }