1 files changed, 59 insertions, 15 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9d61e5ef8..4006a9e08 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
@@ -318,7 +323,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     }
     return;
   }
-
+  
   bool stillNeedToPrintParams = true;
   bool forceBinary = false; // force N-ary to binary when outputing children
   // operator
@@ -585,6 +590,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::APPLY_SELECTOR_TOTAL:
   case kind::PARAMETRIC_DATATYPE:
     break;
+    
+  //separation
+  case kind::SEP_EMP:
+  case kind::SEP_PTO:
+  case kind::SEP_STAR:
+  case kind::SEP_WAND:out << smtKindString(k) << " "; break;
 
     // quantifiers
   case kind::FORALL:
@@ -834,6 +845,39 @@ static string smtKindString(Kind k) throw() {
   case kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv";
   case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real";
 
+  //string theory
+  case kind::STRING_CONCAT: return "str.++";
+  case kind::STRING_LENGTH: return "str.len";
+  case kind::STRING_SUBSTR: return "str.substr" ;
+  case kind::STRING_STRCTN: return "str.contains" ;
+  case kind::STRING_CHARAT: return "str.at" ;
+  case kind::STRING_STRIDOF: return "str.indexof" ;
+  case kind::STRING_STRREPL: return "str.replace" ;
+  case kind::STRING_PREFIX: return "str.prefixof" ;
+  case kind::STRING_SUFFIX: return "str.suffixof" ;
+  case kind::STRING_ITOS: return "int.to.str" ;
+  case kind::STRING_STOI: return "str.to.int" ;
+  case kind::STRING_U16TOS: return "u16.to.str" ;
+  case kind::STRING_STOU16: return "str.to.u16" ;
+  case kind::STRING_U32TOS: return "u32.to.str" ;
+  case kind::STRING_STOU32: return "str.to.u32" ;
+  case kind::STRING_IN_REGEXP: return "str.in.re";
+  case kind::STRING_TO_REGEXP: return "str.to.re";
+  case kind::REGEXP_CONCAT: return "re.++";
+  case kind::REGEXP_UNION: return "re.union";
+  case kind::REGEXP_INTER: return "re.inter";
+  case kind::REGEXP_STAR: return "re.*";
+  case kind::REGEXP_PLUS: return "re.+";
+  case kind::REGEXP_OPT: return "re.opt";
+  case kind::REGEXP_RANGE: return "re.range";
+  case kind::REGEXP_LOOP: return "re.loop";
+  
+  //sep theory
+  case kind::SEP_STAR: return "sep";
+  case kind::SEP_PTO: return "pto";
+  case kind::SEP_WAND: return "wand";
+  case kind::SEP_EMP: return "emp";
+    
   default:
     ; /* fall through */
   }