minor fix

3 files changed, 9 insertions, 18 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b1e37f85e..cf24ae82c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1252,8 +1252,8 @@ builtinOp[CVC4::Kind& kind]
   | STRCON_TOK     { $kind = CVC4::kind::STRING_CONCAT; }
   | STRLEN_TOK     { $kind = CVC4::kind::STRING_LENGTH; }
   | STRSUB_TOK     { $kind = CVC4::kind::STRING_SUBSTR; }
-//  | STRCTN_TOK     { $kind = CVC4::kind::STRING_STRCTN; }
-//  | STRCAT_TOK     { $kind = CVC4::kind::STRING_CHARAT; }
+  | STRCTN_TOK     { $kind = CVC4::kind::STRING_STRCTN; }
+  | STRCAT_TOK     { $kind = CVC4::kind::STRING_CHARAT; }
   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
   | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
   | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 355b182c9..111c4f51d 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -144,18 +144,21 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			std::vector< Node > or_vec;
 			or_vec.push_back( w.eqNode(y) );
 			Node x1 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
-			Node c1 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND,
+			Node b1 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, x1 );
+			Node c1 = NodeManager::currentNM()->mkNode( kind::EXISTS, b1, NodeManager::currentNM()->mkNode( kind::AND,
 							x1.eqNode( emptyString ).negate(),
 							w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x1, y ) )));
 			or_vec.push_back( c1 );
 			Node z2 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
-			Node c2 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND,
+			Node b2 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, z2 );
+			Node c2 = NodeManager::currentNM()->mkNode( kind::EXISTS, b2, NodeManager::currentNM()->mkNode( kind::AND,
 							z2.eqNode( emptyString ).negate(),
 							w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, z2 ) )));
 			or_vec.push_back( c2 );
 			Node x3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
 			Node z3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
-			Node c3 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND,
+			Node b3 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, x3, z3 );
+			Node c3 = NodeManager::currentNM()->mkNode( kind::EXISTS, b3, NodeManager::currentNM()->mkNode( kind::AND,
 							x3.eqNode( emptyString ).negate(), z3.eqNode( emptyString ).negate(),
 							w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x3, y, z3 ) )));
 			or_vec.push_back( c3 );
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index df9d29f0f..9d3197517 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -57,9 +57,6 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
-		if(n.getNumChildren() != 1) {
-          throw TypeCheckingExceptionPrivate(n, "expecting 1 term in string length");
-		}
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
@@ -74,9 +71,6 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
-		if(n.getNumChildren() != 3) {
-          throw TypeCheckingExceptionPrivate(n, "expecting 3 terms in substr");
-		}
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
@@ -99,9 +93,6 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
-		if(n.getNumChildren() != 2) {
-          throw TypeCheckingExceptionPrivate(n, "expecting 2 terms in string contain");
-		}
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
@@ -111,7 +102,7 @@ public:
           throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain");
         }
     }
-    return nodeManager->stringType();
+    return nodeManager->booleanType();
   }
 };
 
@@ -120,9 +111,6 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
-		if(n.getNumChildren() != 2) {
-          throw TypeCheckingExceptionPrivate(n, "expecting 2 terms in string char at");
-		}
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at");