From 20250b200f472006e51d6d6bca3dec49821d5d51 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Sep 2022 20:31:36 -0700 Subject: [PATCH] #6319 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_internalize.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 609f5296b..c8ae2a7c6 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -266,7 +266,7 @@ namespace euf { return; sort* srt = e->get_arg(0)->get_sort(); auto sort_sz = srt->get_num_elements(); - if (sort_sz.is_finite() && sort_sz.size() <= sz) + if (sort_sz.is_finite() && sort_sz.size() < sz) s().add_clause(0, nullptr, st); else if (sz <= distinct_max_args) { for (unsigned i = 0; i < sz; ++i) {