mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

patching crash in data-type factory when fresh values are not produced

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-15 04:37:05 -07:00
parent be044f42c3
commit 21b27cd2d1
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/proto_model/datatype_factory.cpp
View file

@ -67,6 +67,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
value_set * set = get_value_set(s);
if (set->empty()) {
expr * val = get_some_value(s);
SASSERT(val);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, val);
return val;
@ -185,10 +186,16 @@ expr * datatype_factory::get_fresh_value(sort * s) {
if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
found_sibling = true;
expr * maybe_new_arg = get_almost_fresh_value(s_arg);
if (!maybe_new_arg) {
maybe_new_arg = m_model.get_some_value(s_arg);
found_sibling = false;
}
SASSERT(maybe_new_arg);
args.push_back(maybe_new_arg);
}
else {
expr * some_arg = m_model.get_some_value(s_arg);
SASSERT(some_arg);
args.push_back(some_arg);
}
}