From aa5267cb9c585e1d6d21397f21ea7e6c700c231b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Mar 2026 10:28:21 -0700 Subject: [PATCH] Add comments for large exponent handling Add comments for handling large exponents in seq_model.cpp --- src/smt/seq/seq_model.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/smt/seq/seq_model.cpp b/src/smt/seq/seq_model.cpp index a13406201..caca1e4cc 100644 --- a/src/smt/seq/seq_model.cpp +++ b/src/smt/seq/seq_model.cpp @@ -258,6 +258,9 @@ namespace smt { zstring result(buf.size(), buf.data()); return expr_ref(m_seq.str.mk_string(result), m); } + // NSB review: just return an expression of the form: + // mk_power(base_val, a.mk_int(n_val)) for large exponents + // Fallback: cap exponent to avoid divergence n_val = POWER_EXPAND_LIMIT; }