mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 21:50:52 +00:00
Code Activity

One check was missing

Browse source
This commit is contained in:
CEisenhofer 2024-12-27 14:54:27 +01:00
parent 9d7ce8e779
commit 1cd5e22d66
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -715,6 +715,7 @@ namespace sls {
if (is_value(x)) if (is_value(x))
break; break;
auto new_val = val_x.extract(0, first_diff) + zstring(val_other[first_diff]) + val_x.extract(first_diff + 1, val_x.length()); auto new_val = val_x.extract(0, first_diff) + zstring(val_other[first_diff]) + val_x.extract(first_diff + 1, val_x.length());
if (val_x != new_val)
m_str_updates.push_back({ x, new_val, 1 }); m_str_updates.push_back({ x, new_val, 1 });
break; break;
} }
@ -1622,8 +1623,9 @@ namespace sls {
} }
bool seq_plugin::update(expr* e, zstring const& value) { bool seq_plugin::update(expr* e, zstring const& value) {
if (value == strval0(e)) SASSERT(value != strval0(e));
return true; // if (value == strval0(e))
// return true;
if (is_value(e)) if (is_value(e))
return false; return false;
if (get_eval(e).min_length > value.length() || get_eval(e).max_length < value.length()) if (get_eval(e).min_length > value.length() || get_eval(e).max_length < value.length())