mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-02 15:17:54 +00:00
Code Activity

Extract argument of unit when adding constant character to range

Browse source
This commit is contained in:
CEisenhofer 2026-04-21 18:54:36 +02:00
parent 8b2643ff02
commit 46364a1502
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/seq/seq_nielsen.cpp
View file

@ -350,7 +350,9 @@ namespace seq {
// for a concrete character just check if it matches // for a concrete character just check if it matches
expr* val = sym_char->get_expr(); expr* val = sym_char->get_expr();
unsigned ch; 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++) { for (unsigned i = 0; i < range.ranges().size(); i++) {
if (range.ranges()[i].contains(ch)) if (range.ranges()[i].contains(ch))
return; // matches, no conflict return; // matches, no conflict