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

Small seq-sls fixes (#7503)

Browse source 
* Calculation based on wrong update list

* Fixed regex problem
This commit is contained in:
Clemens Eisenhofer 2025-01-07 18:26:00 +01:00 committed by GitHub
parent e133a297ba
commit 5c60c6662c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

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

@ -1676,7 +1676,7 @@ namespace sls {
if (!is_str_update) { if (!is_str_update) {
i = m_int_updates.size(); i = m_int_updates.size();
do { do {
lim -= m_str_updates[--i].m_score; lim -= m_int_updates[--i].m_score;
} while (lim >= 0 && i > 0); } while (lim >= 0 && i > 0);
} }
@ -2066,7 +2066,13 @@ namespace sls {
return append_char(r0, r, s); 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)) { if (m.is_ite(r, c, th, el)) {
unsigned low = 0, high = UINT_MAX; unsigned low = 0, high = UINT_MAX;