From ab259b683072b45fc06bd273a95ec896f312c341 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 31 May 2026 17:41:34 -0700 Subject: [PATCH] add depth guard --- src/model/datatype_factory.cpp | 3 +++ src/model/datatype_factory.h | 2 ++ 2 files changed, 5 insertions(+) diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index b93703acd..fac858ccc 100644 --- a/src/model/datatype_factory.cpp +++ b/src/model/datatype_factory.cpp @@ -139,6 +139,9 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) { expr * datatype_factory::get_fresh_value(sort * s) { if (!m_util.is_datatype(s)) return m_model.get_fresh_value(s); + if (m_fresh_depth >= m_max_fresh_depth) + return get_last_fresh_value(s); + struct depth_guard { unsigned& d; depth_guard(unsigned& d) : d(d) { ++d; } ~depth_guard() { --d; } } _dg(m_fresh_depth); TRACE(datatype, tout << "generating fresh value for: " << s->get_name() << "\n";); auto& [set, values] = get_value_set(s); // Approach 0) diff --git a/src/model/datatype_factory.h b/src/model/datatype_factory.h index b2a6b75d3..2d8f216b4 100644 --- a/src/model/datatype_factory.h +++ b/src/model/datatype_factory.h @@ -24,6 +24,8 @@ Revision History: class datatype_factory : public struct_factory { datatype_util m_util; obj_map m_last_fresh_value; + unsigned m_fresh_depth = 0; + static const unsigned m_max_fresh_depth = 512; expr * get_last_fresh_value(sort * s); expr * get_almost_fresh_value(sort * s);