From 2264fce7c63ddf142635ed3be83551d30f7a1a32 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 24 Feb 2014 11:36:23 -0600 Subject: [PATCH] bug fix: strings preprocess for the orignal term, causing unknown in some cases --- src/theory/strings/theory_strings_preprocess.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); -- 2.30.2