From 88bd01bc4fabb2800b3abfe6badf2bd3ae0fa68e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Jun 2014 23:03:34 +0530 Subject: [PATCH] patching non-termination bug in datatype factory, reported by Tiago Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/datatype_factory.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp index 5e66ab738..3b0ec8e5f 100644 --- a/src/smt/proto_model/datatype_factory.cpp +++ b/src/smt/proto_model/datatype_factory.cpp @@ -191,8 +191,10 @@ expr * datatype_factory::get_fresh_value(sort * s) { // Approach 2) // For recursive datatypes. // search for constructor... + unsigned num_iterations = 0; if (m_util.is_recursive(s)) { while(true) { + ++num_iterations; TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";); ptr_vector const * constructors = m_util.get_datatype_constructors(s); ptr_vector::const_iterator it = constructors->begin(); @@ -212,7 +214,13 @@ expr * datatype_factory::get_fresh_value(sort * s) { << found_sibling << "\n";); 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); + expr * maybe_new_arg = 0; + if (num_iterations <= 1) { + maybe_new_arg = get_almost_fresh_value(s_arg); + } + else { + maybe_new_arg = get_fresh_value(s_arg); + } if (!maybe_new_arg) { TRACE("datatype_factory", tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";); @@ -231,6 +239,7 @@ expr * datatype_factory::get_fresh_value(sort * s) { if (found_sibling) { expr_ref new_value(m_manager); new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr()); + TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";); m_last_fresh_value.insert(s, new_value); if (!set->contains(new_value)) { register_value(new_value);