From 46364a150286a21df0c6ef8eb3eac1ff91909f00 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 21 Apr 2026 18:54:36 +0200 Subject: [PATCH] Extract argument of unit when adding constant character to range --- src/smt/seq/seq_nielsen.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 98f3b0696..4921d29fd 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -350,7 +350,9 @@ namespace seq { // for a concrete character just check if it matches expr* val = sym_char->get_expr(); unsigned ch; - VERIFY(graph().seq().is_const_char(val, ch)); + expr* ch_expr; + VERIFY(graph().seq().str.is_unit(val, ch_expr)); + VERIFY(graph().seq().is_const_char(ch_expr, ch)); for (unsigned i = 0; i < range.ranges().size(); i++) { if (range.ranges()[i].contains(ch)) return; // matches, no conflict