From 866d97f768b0ed0217e66b30762bf6e6aa4ff5ca Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 17 May 2016 16:45:53 -0400 Subject: [PATCH] fix eval_concat copy-and-paste error in simplify_parent; concat-eq-concat-case3_sat now passing --- src/smt/theory_str.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index ff0aacfa1..4c936dea5 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -963,7 +963,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { // (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) { bool arg0HasEqcValue = false; expr * arg0Value = get_eqc_value(arg0, arg0HasEqcValue);