mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix constant eqc bug in mk_concat

Browse source
This commit is contained in:
Murphy Berzish 2018-01-24 22:02:00 -05:00
parent d648f95f63
commit 8d5065d35d
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_str.cpp
View file

@ -709,6 +709,12 @@ namespace smt {
bool n2HasEqcValue = false;
expr * v1 = get_eqc_value(n1, n1HasEqcValue);
expr * v2 = get_eqc_value(n2, n2HasEqcValue);
if (u.str.is_string(v1)) {
n1HasEqcValue = true;
}
if (u.str.is_string(v2)) {
n2HasEqcValue = true;
}
if (n1HasEqcValue && n2HasEqcValue) {
zstring n1_str;
u.str.is_string(v1, n1_str);