diff options
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 18 |
1 files changed, 4 insertions, 14 deletions
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 9ffe9150d..6d3a12cc4 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -306,9 +306,7 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { - TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); - TypeNode t = (*it).getType(check); + TypeNode t = n[0].getType(check); if (!t.isRegExp()) { throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); } @@ -322,9 +320,7 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { - TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); - TypeNode t = (*it).getType(check); + TypeNode t = n[0].getType(check); if (!t.isRegExp()) { throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); } @@ -338,9 +334,7 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { - TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); - TypeNode t = (*it).getType(check); + TypeNode t = n[0].getType(check); if (!t.isRegExp()) { throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); } @@ -355,7 +349,6 @@ public: throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); char ch[2]; for(int i=0; i<2; ++i) { @@ -421,9 +414,7 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { - TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); - TypeNode t = (*it).getType(check); + TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting string terms"); } @@ -441,7 +432,6 @@ public: throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); TypeNode t = (*it).getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting string terms"); |