mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix bug found by Ethan: fresh values for bit-vectors loops if the domain of bit-vectors is truly small

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-13 15:30:56 -07:00
parent 10e203da43
commit 419f99c329
4 changed files with 18 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/proto_model/value_factory.h
View file

@ -180,10 +180,24 @@ public:
value_set * set = get_value_set(s);
bool is_new = false;
expr * result = 0;
sort_info* s_info = s->get_info();
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<unsigned>(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) {
return 0;
}
}
SASSERT(result != 0);
return result;