From 9c36e9ce62dead267387c8b8fb80de246e821825 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Mar 2026 10:30:12 -0700 Subject: [PATCH] Revise comments for clarity on sort usage Updated comments to reflect review suggestions regarding the use of the sort of 'n'. --- 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 caca1e4cc..a2e6900b3 100644 --- a/src/smt/seq/seq_model.cpp +++ b/src/smt/seq/seq_model.cpp @@ -158,6 +158,7 @@ namespace smt { if (!n) return expr_ref(m); + // NSB review: use the sort of n if (n->is_empty()) return expr_ref(m_seq.str.mk_empty(m_seq.str.mk_string_sort()), m); @@ -228,6 +229,8 @@ namespace smt { exp_val = rational(0); // Build the repeated string: base^exp_val + + // NSB review: use the sort of n instead of mk_string_sort() if (exp_val.is_zero()) return expr_ref(m_seq.str.mk_empty(m_seq.str.mk_string_sort()), m); if (exp_val.is_one())