diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-24 11:36:23 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-24 11:36:23 -0600 |
| commit | 2264fce7c63ddf142635ed3be83551d30f7a1a32 (patch) | |
| tree | 2571622a801cbb82e4d8dc1d7a7dc4e41f92f012 /src/theory | |
| parent | 5ceb5dc2f83d29b27afb578c64a20274fed13c86 (diff) | |
bug fix: strings preprocess for the orignal term, causing unknown in some cases
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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); |