mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 08:17:37 +00:00
Code Activity

Fixed regex problem

Browse source
This commit is contained in:
CEisenhofer 2025-01-07 11:01:07 +01:00
parent b765225ed8
commit 2d10779f4a
2 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -653,7 +653,6 @@ namespace sls {
return false;
SASSERT(is_uninterp(t));
SASSERT(m_restore.empty());
if (bv.is_bv(t)) {
wval(t).eval = new_value;

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

@ -2066,7 +2066,13 @@ namespace sls {
return append_char(r0, r, s);
}
}
NOT_IMPLEMENTED_YET();
expr* r2;
do {
r2 = to_app(r)->get_arg(ctx.rand(to_app(r)->get_num_args()));
} while (r2 == r0);
r = r2;
// Just take one that is not a self loop (there is always such one element)
return append_char(r0, r, s);
}
if (m.is_ite(r, c, th, el)) {
unsigned low = 0, high = UINT_MAX;