From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Sat, 25 Jan 2014 04:32:45 +0000 (-0600)
Subject: minor fix, indexof rewriter opt
X-Git-Tag: cvc5-1.0.0~7123
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa24a2bf6b511c4db580ded8cd4dec0792a1b392;p=cvc5.git

minor fix, indexof rewriter opt
---

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1d55fb193..11642a4d2 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -267,11 +267,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y );
 			Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) );
 			Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) );
-			Node iof = NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, x, y, zero );
-			Node c3 = iof.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-			Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond,
+			Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, sk1, y ).negate();
+			Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
 							NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 ),
-							skw.eqNode(x) );
+							skw.eqNode(x) ) );
 			new_nodes.push_back( rr );
 			d_cache[t] = skw;
 			retNode = skw;