Cleanup from last commit, treat sep.nil as variable kind.

2 files changed, 6 insertions, 8 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b3fe59b79..29d3e45b6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1607,10 +1607,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         Debug("parser") << "Empty set encountered: " << f << " "
                           << f2 << " " << type <<  std::endl;
         expr = MK_CONST( ::CVC4::EmptySet(type) );
-      } else if(f.getKind() == CVC4::kind::NIL_REF) {
-        //hack: We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational.
-        //      However, the expression has 0 children. So we convert to (sep_nil tmp) here.
-        expr = MK_EXPR(CVC4::kind::SEP_NIL, PARSER_STATE->mkBoundVar("__tmp",type) );        
+      } else if(f.getKind() == CVC4::kind::SEP_NIL_REF) {
+        //We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational.
+        //However, the expression has 0 children. So we convert to a SEP_NIL variable.
+        expr = EXPR_MANAGER->mkSepNil(type);
       } else {
         if(f.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 90fc11803..a46eae475 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -167,16 +167,14 @@ void Smt2::addFloatingPointOperators() {
 }
 
 void Smt2::addSepOperators() {
-  //addOperator(kind::SEP_NIL, "sep.nil");
   addOperator(kind::SEP_STAR, "sep");
   addOperator(kind::SEP_PTO, "pto");
   addOperator(kind::SEP_WAND, "wand");
-  addOperator(kind::EMP_STAR, "emp");
-  //Parser::addOperator(kind::SEP_NIL);
+  addOperator(kind::SEP_EMP, "emp");
   Parser::addOperator(kind::SEP_STAR);
   Parser::addOperator(kind::SEP_PTO);
   Parser::addOperator(kind::SEP_WAND);
-  Parser::addOperator(kind::EMP_STAR);
+  Parser::addOperator(kind::SEP_EMP);
 }
 
 void Smt2::addTheory(Theory theory) {