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

1 files changed, 21 insertions, 21 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7b6bc8708..35e6f1a73 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -117,21 +117,26 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
 
   // variable
   if(n.isVar()) {
-    string s;
-    if(n.getAttribute(expr::VarNameAttr(), s)) {
-      out << maybeQuoteSymbol(s);
-    } else {
-      if(n.getKind() == kind::VARIABLE) {
-        out << "var_";
+    if( n.getKind() == kind::SEP_NIL ){
+      out << "(as sep.nil " << n.getType() << ")";
+      return;
+    }else{
+      string s;
+      if(n.getAttribute(expr::VarNameAttr(), s)) {
+        out << maybeQuoteSymbol(s);
       } else {
-        out << n.getKind() << '_';
+        if(n.getKind() == kind::VARIABLE) {
+          out << "var_";
+        } else {
+          out << n.getKind() << '_';
+        }
+        out << n.getId();
+      }
+      if(types) {
+        // print the whole type, but not *its* type
+        out << ":";
+        n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
       }
-      out << n.getId();
-    }
-    if(types) {
-      // print the whole type, but not *its* type
-      out << ":";
-      n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
     }
 
     return;
@@ -291,7 +296,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     case kind::EMPTYSET:
       out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
       break;
-
+  
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant
@@ -319,11 +324,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     return;
   }
   
-  if( n.getKind() == kind::SEP_NIL ){
-    out << "sep.nil";
-    return;
-  }
-  
   bool stillNeedToPrintParams = true;
   bool forceBinary = false; // force N-ary to binary when outputing children
   // operator
@@ -588,7 +588,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     break;
     
   //separation
-  case kind::EMP_STAR:
+  case kind::SEP_EMP:
   case kind::SEP_PTO:
   case kind::SEP_STAR:
   case kind::SEP_WAND:out << smtKindString(k) << " "; break;
@@ -868,7 +868,7 @@ static string smtKindString(Kind k) throw() {
   case kind::SEP_STAR: return "sep";
   case kind::SEP_PTO: return "pto";
   case kind::SEP_WAND: return "wand";
-  case kind::EMP_STAR: return "emp";
+  case kind::SEP_EMP: return "emp";
     
   default:
     ; /* fall through */