mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 11:35:42 +00:00
Code Activity

bug fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-03 19:50:19 -07:00
parent 52e6f885b9
commit d19f19c5d6
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/seq_regex.cpp
View file

@ -510,9 +510,10 @@ namespace smt {
expr *e = ctx.bool_var2expr(lit.var());
VERIFY(str().is_in_re(e, s, r));
expr_ref_vector prefix(m);
expr *hd, *v, *tl = s;
while (str().is_concat(tl, hd, tl) && str().is_unit(hd, v) && m.is_value(v))
prefix.push_back(v);
expr *hd, *v, *tl = s, *tl1;
while (str().is_concat(tl, hd, tl1) && str().is_unit(hd, v) && m.is_value(v))
prefix.push_back(v),
tl = tl1;
if (prefix.empty())
return false;