From 8c02ec087b8fb19d5cc793794e0fad42f8b7283f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 May 2026 10:53:12 -0700 Subject: [PATCH] fix crash with D:\\bench\\inputs\\QF_S\\20240318-omark\\cyclic-xy.smt2 Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.h | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 303ee8d21..caa1d76da 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -640,7 +640,12 @@ namespace seq { bool upper_bound(expr* e, rational& up, dep_tracker& dep); // character constraint access (mirrors ZIPT's CharRanges) - u_map> char_ranges() const { return m_char_ranges; } + u_map>& char_ranges() { return m_char_ranges; } + u_map> const &char_ranges() const { + return m_char_ranges; + } + + // add a character range constraint for a symbolic char. // intersects with existing range; sets conflict if result is empty.