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 964f5d8e1df3e5e2531255ab9d67a22925c17cf7..43d3bfe47a69f76f4e36ec6dc7a7f4ec4576871c 100644 (file)
--- 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);