From 2df5b1632d48df1d526bb14ea31f3cb84defb5a6 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 15 Apr 2015 23:21:52 -0400
Subject: [PATCH] array theory builtinop

---
 src/parser/smt2/Smt2.g   | 5 -----
 src/parser/smt2/smt2.cpp | 4 ++--
 2 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8196a6276..dfbb79d72 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2044,9 +2044,6 @@ builtinOp[CVC4::Kind& kind]
   | TO_INT_TOK   { $kind = CVC4::kind::TO_INTEGER; }
   | TO_REAL_TOK  { $kind = CVC4::kind::TO_REAL; }
 
-  | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
-  | STORE_TOK    { $kind = CVC4::kind::STORE; }
-
   | BV2NAT_TOK     { $kind = CVC4::kind::BITVECTOR_TO_NAT;
                      if(PARSER_STATE->strictModeEnabled()) {
                        PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
@@ -2474,9 +2471,7 @@ OR_TOK            : 'or';
 // PERCENT_TOK       : '%';
 PLUS_TOK          : '+';
 //POUND_TOK         : '#';
-SELECT_TOK        : 'select';
 STAR_TOK          : '*';
-STORE_TOK         : 'store';
 // TILDE_TOK         : '~';
 TO_INT_TOK        : 'to_int';
 TO_REAL_TOK       : 'to_real';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index bc1f94f36..a782bf1ba 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -135,8 +135,8 @@ void Smt2::addFloatingPointOperators() {
 void Smt2::addTheory(Theory theory) {
   switch(theory) {
   case THEORY_ARRAYS:
-    Parser::addOperator(kind::SELECT);
-    Parser::addOperator(kind::STORE);
+    addOperator(kind::SELECT, "select");
+    addOperator(kind::STORE, "store");
     break;
 
   case THEORY_BITVECTORS:
-- 
2.30.2