mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 19:47:52 +00:00
Code Activity

Guarded index check

Browse source
This commit is contained in:
CEisenhofer 2024-12-30 17:30:12 +01:00
parent 7c02410e52
commit d54e54580d
1 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/sls/sls_seq_plugin.cpp
View file

@ -1480,6 +1480,19 @@ namespace sls {
VERIFY(a.is_numeral(len_e, len_val)); VERIFY(a.is_numeral(len_e, len_val));
if (v.empty() && (offset_val.is_neg() || !len_val.is_pos())) if (v.empty() && (offset_val.is_neg() || !len_val.is_pos()))
return true; return true;
if (offset_val.is_neg() || offset_val.get_unsigned() >= r.length()) {
m_str_updates.push_back({ e, zstring(), 1 });
for (unsigned i = 0; i < r.length(); i++)
m_int_updates.push_back({ offset, rational(i), 1 });
return apply_update();
}
if (!len_val.is_pos()) {
m_str_updates.push_back({ e, zstring(), 1 });
for (unsigned i = 0; i < r.length() - offset_val.get_unsigned(); i++)
m_int_updates.push_back({ len, rational(i), 1 });
return apply_update();
}
if (v == r.extract(offset_val.get_unsigned(), len_val.get_unsigned())) if (v == r.extract(offset_val.get_unsigned(), len_val.get_unsigned()))
return true; return true;