mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

fix eval_concat copy-and-paste error in simplify_parent; concat-eq-concat-case3_sat now passing

Browse source
This commit is contained in:
Murphy Berzish 2016-05-17 16:45:53 -04:00
parent 2f80a9d4ae
commit 866d97f768
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -963,7 +963,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) {
// (Concat arg0 n_eqNode) /\ arg0 has eq const // (Concat arg0 n_eqNode) /\ arg0 has eq const
expr * concatResult = eval_concat(eq_str, arg1); expr * concatResult = eval_concat(arg0, eq_str);
if (concatResult != NULL) { if (concatResult != NULL) {
bool arg0HasEqcValue = false; bool arg0HasEqcValue = false;
expr * arg0Value = get_eqc_value(arg0, arg0HasEqcValue); expr * arg0Value = get_eqc_value(arg0, arg0HasEqcValue);