From a0ba95098761a0f31191e6d9b593c026c0856c72 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2026 11:19:53 -0700 Subject: [PATCH] fix type errors Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 2 ++ src/smt/seq_model.cpp | 7 ++++--- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index a47154e71..462f8a32e 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -3833,6 +3833,8 @@ namespace seq { for (unsigned i = 0; i < substs.size(); ++i) { auto const& s = substs[i]; SASSERT(s.m_var && s.m_var->is_var()); + if (!m_seq.is_seq(s.m_var->get_expr())) + continue; expr_ref lhs = compute_length_expr(s.m_var); lhs_exprs.push_back({i, lhs.get()}); if (s.is_eliminating()) diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index 80400cd0e..78b7e3f4a 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -294,9 +294,10 @@ namespace smt { } expr* seq_model::mk_fresh_value(euf::snode* var) { - sort* srt = m_seq.str.mk_string_sort(); - if (var->get_expr()) - srt = var->get_expr()->get_sort(); + SASSERT(var->get_expr()); + if (!m_seq.is_seq(var->get_expr())) + return nullptr; + auto srt = var->get_expr()->get_sort(); // check if this variable has regex constraints euf::snode* re = nullptr;