From 5e3a6d0af7438d655ea7f53fc1fd40eb7051ed7a Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 27 Jul 2015 20:56:46 -0500 Subject: [PATCH] minor change to the last fix --- 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 b27cab223..12b6bc53b 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -196,7 +196,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) ); Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero); - Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero); + Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GT, t[2], d_zero); Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" ); Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" ); -- 2.30.2