From c54929e59f7cbeaaa25f64c47cb78e5f4a6d6906 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Sep 2013 04:52:21 -0700 Subject: [PATCH] cycle through domain size before giving up Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/value_factory.h | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/smt/proto_model/value_factory.h b/src/smt/proto_model/value_factory.h index 115a01345..5bd0a1f75 100644 --- a/src/smt/proto_model/value_factory.h +++ b/src/smt/proto_model/value_factory.h @@ -184,18 +184,16 @@ public: sort_size const* sz = s_info?&s_info->get_num_elements():0; bool has_max = false; Number max_size; - if (sz && sz->is_finite()) { - if (sz->size() < UINT_MAX) { - unsigned usz = static_cast(sz->size()); - max_size = Number(usz); - has_max = true; - } + if (sz && sz->is_finite() && sz->size() < UINT_MAX) { + unsigned usz = static_cast(sz->size()); + max_size = Number(usz); + has_max = true; } Number & next = set->m_next; while (!is_new) { result = mk_value(next, s, is_new); next++; - if (has_max && next >= max_size) { + if (has_max && next > max_size + set->m_next) { return 0; } }