From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sun, 8 Jun 2014 23:35:39 +0000 (-0400)
Subject: smt2 parser: tokenize emptyset only if theory enabled
X-Git-Tag: cvc5-1.0.0~6847^2~2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9978c259f30b1f4b2c70c04589a309033a6eb1f6;p=cvc5.git

smt2 parser: tokenize emptyset only if theory enabled
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b3761dfbd..bc417d54c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1778,10 +1778,10 @@ REALLCHAR_TOK : 're.allchar';
 
 FMFCARD_TOK : 'fmf.card';
 
-EMPTYSET_TOK: 'emptyset'; // Other set theory operators are not
-                          // tokenized and handled directly when
-                          // processing a term
-
+EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
+// Other set theory operators are not
+// tokenized and handled directly when
+// processing a term
 
 /**
  * A sequence of printable ASCII characters (except backslash) that starts