mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

fix #2830

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-26 14:41:09 -08:00
parent 914856b9ba
commit 1d77e3e19f
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/bool_rewriter.cpp
View file

@ -752,7 +752,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
if (!m().is_unique_value(arg)) if (!m().is_unique_value(arg))
all_value = false; all_value = false;
if (!all_value && all_diff) { 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]); all_diff = m().are_distinct(arg, args[j]);
} }
} }