mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-23 04:49:11 +00:00
Code Activity

Missing range cases

Browse source
This commit is contained in:
CEisenhofer 2026-03-20 10:41:56 +01:00
parent d77e9d5c95
commit 3662b89adc
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -370,7 +370,7 @@ namespace seq {
if (re->is_fail())
return true;
// kinds that are never empty
if (re->is_star() || re->is_to_re() ||
if (re->is_star() || re->is_to_re() || re->is_range() ||
re->is_full_char() || re->is_full_seq())
return false;
// loop with lo == 0 accepts ε
@ -509,7 +509,7 @@ namespace seq {
if (re->is_nullable())
return l_false;
// Structural quick checks for kinds that are never empty
if (re->is_star() || re->is_full_char() || re->is_full_seq() || re->is_to_re())
if (re->is_star() || re->is_full_char() || re->is_full_seq() || re->is_to_re() || re->is_range())
return l_false;
// Structural emptiness catches simple cases
if (is_empty_regex(re))