mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-21 03:42:04 +00:00
Code Activity

another stab at fixing substring interval extraction combinatorics

Browse source 
- i is the offset into val_other. The valid offsets are 0... |val_other|-1.
- j is the length of the substring. It only makes sense to extract strings of length 1,... |val_other|-i
This commit is contained in:
Nikolaj Bjorner 2025-01-12 11:14:17 -08:00
parent fa22b646aa
commit 558758fcf1
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -694,7 +694,7 @@ namespace sls {
hashtable<zstring, zstring_hash_proc, default_eq<zstring>> set; hashtable<zstring, zstring_hash_proc, default_eq<zstring>> set;
set.insert(zstring("")); set.insert(zstring(""));
for (unsigned i = 0; i < val_other.length(); ++i) { for (unsigned i = 0; i < val_other.length(); ++i) {
for (unsigned j = val_other.length() - i; j-- > 0; ) { for (unsigned j = 1; j <= val_other.length() - i; ++j) {
zstring sub = val_other.extract(i, j); zstring sub = val_other.extract(i, j);
if (set.contains(sub)) if (set.contains(sub))
break; break;