From 191c50b529310cae9f39463d371eb92b896560d5 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 29 Sep 2015 17:52:19 -0400
Subject: [PATCH] fix solve_concat_eq_str() case 4: prefixStr should have been
 suffixStr

---
 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 e2896f4f5..f9fb7e3a4 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -622,7 +622,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) {
         				expr_ref arg1_eq (ctx.mk_eq_atom(arg1, prefixAst), m);
         				and_items[and_count++] = ctx.mk_eq_atom(xorAst, arg1_eq);
 
-        				expr_ref suffixAst(m_strutil.mk_string(prefixStr), m);
+        				expr_ref suffixAst(m_strutil.mk_string(suffixStr), m);
         				expr_ref arg2_eq (ctx.mk_eq_atom(arg2, suffixAst), m);
         				and_items[and_count++] = ctx.mk_eq_atom(xorAst, arg2_eq);
         			}