From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 24 Feb 2014 17:36:23 +0000 (-0600)
Subject: bug fix: strings preprocess for the orignal term, causing unknown in some cases
X-Git-Tag: cvc5-1.0.0~7068
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2264fce7c63ddf142635ed3be83551d30f7a1a32;p=cvc5.git

bug fix: strings preprocess for the orignal term, causing unknown in some cases
---

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 964f5d8e1..43d3bfe47 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -536,7 +536,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
 	} else if(num == 1) {
 		Node s = decompose(t[0], new_nodes);
 		if(s != t[0]) {
-			Node tmp = NodeManager::currentNM()->mkNode( t.getKind(), t[0] );
+			Node tmp = NodeManager::currentNM()->mkNode( t.getKind(), s );
 			return simplify(tmp, new_nodes);
 		} else {
 			return simplify(t, new_nodes);