From 5be4365b47fe518ddbe3583ce8c3449567c4ab7d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Sep 2013 16:53:52 -0700 Subject: [PATCH] redo edit Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/value_factory.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/proto_model/value_factory.h b/src/smt/proto_model/value_factory.h index 5bd0a1f75..92ad2373b 100644 --- a/src/smt/proto_model/value_factory.h +++ b/src/smt/proto_model/value_factory.h @@ -189,11 +189,12 @@ public: max_size = Number(usz); has_max = true; } + Number start = set->m_next; Number & next = set->m_next; while (!is_new) { result = mk_value(next, s, is_new); next++; - if (has_max && next > max_size + set->m_next) { + if (has_max && next > max_size + start) { return 0; } }