From af2769dbc0360605b6ad9edeb4e6fcad3016d422 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 May 2026 14:07:49 -0700 Subject: [PATCH] more logging for when arith_value fails Signed-off-by: Nikolaj Bjorner --- src/smt/seq_model.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index bc8f71d68..7fd890813 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -513,6 +513,7 @@ namespace smt { expr_ref len_expr(m_seq.str.mk_length(var->get_expr()), m); rational len_val; bool has_len = avalue.get_value(len_expr, len_val); + CTRACE(seq, !has_len, tout << "no value associated with " << mk_pp(len_expr, m) << "\n";); if (has_len && len_val.is_unsigned()) { unsigned n = len_val.get_unsigned(); @@ -542,6 +543,7 @@ namespace smt { arith_value avalue(m); avalue.init(&m_ctx); bool has_len = avalue.get_value(len_expr, len_val); + CTRACE(seq, !has_len, tout << "no value associated with " << mk_pp(len_expr, m) << "\n";); if (has_len) {