mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-29 03:48:51 +00:00
Code Activity

Fix uninitialized clo/chi read in mk_re_range; drop disabled test block

Browse source 
mk_re_range read clo/chi in the singleton/ordering checks before the
is_empty guard, but an early is_empty (from the length checks) leaves
them uninitialized. Initialize to 0 and move the is_empty return ahead
of the singleton check so uninitialized values are never used.

Also remove the disabled if(false) range-complement block in the
seq_rewriter unit test.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Margus Veanes 2026-06-26 06:58:41 +03:00
parent 5e38eb328d
commit eab5ff1eff
2 changed files with 11 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/ast/rewriter/seq_rewriter.cpp
View file

@ -4117,7 +4117,7 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
*/
br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
zstring slo, shi;
unsigned clo, chi;
unsigned clo = 0, chi = 0;
expr *lo1, *hi1;
unsigned len = 0;
bool is_empty = false;
@ -4148,20 +4148,23 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
is_empty = true;
}
if (clo > chi)
// clo/chi are only meaningful once both bounds were extracted; an early
// is_empty (from the length checks) leaves them at their default 0, so the
// is_empty return must come before the singleton/ordering checks below.
if (!is_empty && clo > chi)
is_empty = true;
// Singleton: re.range "a" "a" → str.to_re "a"
if (clo == chi) {
result = re().mk_to_re(str().mk_string(zstring(clo)));
return BR_DONE;
}
if (is_empty) {
sort* srt = re().mk_re(lo->get_sort());
result = re().mk_empty(srt);
return BR_DONE;
}
// Singleton: re.range "a" "a" → str.to_re "a"
if (clo == chi) {
result = re().mk_to_re(str().mk_string(zstring(clo)));
return BR_DONE;
}
return BR_FAILED;
}

12
src/test/seq_rewriter.cpp
View file

@ -125,18 +125,6 @@ void tst_seq_rewriter() {
}
// -----------------------------------------------------------------------
// 10. Range complement (lo = 0): single range e union [hi+1, max].*
// -----------------------------------------------------------------------
if (false) {
expr_ref lo_str(su.str.mk_string(zstring(0u)), m);
expr_ref hi_str(su.str.mk_string(zstring((unsigned)'f')), m);
expr_ref e(su.re.mk_complement(su.re.mk_range(lo_str, hi_str)), m);
rw(e);
std::cout << "range comp lo=min: " << mk_pp(e, m) << "\n";
ENSURE(!su.re.is_complement(e));
}
// -----------------------------------------------------------------------
// 11. Downstream: (re.* (re.range "z" "a")) → str.to_re ""
// -----------------------------------------------------------------------