Simplify the syntax and representation of the separation logic empty heap constraint (#7268)

Since ~1 year ago, we insist that the location and data types of the separation logic heap are set upfront, analogous to the set-logic command. This means that the separation logic empty heap constraint does not need to be annotated with its types.

This makes SEP_EMP a nullary Boolean operator instead of binary predicate (taking dummy arguments whose types specify the heap type). It changes the smt2 extended syntax from (_ emp T1 T2) to sep.emp.

25 files changed, 107 insertions, 118 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d33ef5b42..42690586a 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5079,21 +5079,26 @@ Sort Solver::mkTupleSortHelper(const std::vector<Sort>& sorts) const
 
 Term Solver::mkTermFromKind(Kind kind) const
 {
-  CVC5_API_KIND_CHECK_EXPECTED(
-      kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
+  CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY
+                                   || kind == REGEXP_SIGMA || kind == SEP_EMP,
+                               kind)
       << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
   //////// all checks before this line
   Node res;
+  cvc5::Kind k = extToIntKind(kind);
   if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
   {
-    cvc5::Kind k = extToIntKind(kind);
     Assert(isDefinedIntKind(k));
     res = d_nodeMgr->mkNode(k, std::vector<Node>());
   }
+  else if (kind == SEP_EMP)
+  {
+    res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->booleanType(), k);
+  }
   else
   {
     Assert(kind == PI);
-    res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), cvc5::kind::PI);
+    res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), k);
   }
   (void)res.getType(true); /* kick off type checking */
   increment_term_stats(kind);
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 94a8a6f92..0ff05022f 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -2064,17 +2064,10 @@ enum CVC5_EXPORT Kind : int32_t
    */
   SEP_NIL,
   /**
-   * Separation logic empty heap.
-   *
-   * Parameters:
-   *   - 1: Term of the same sort as the sort of the location of the heap
-   *         that is constrained to be empty
-   *   - 2: Term of the same sort as the data sort of the heap that is
-   *         that is constrained to be empty
+   * Separation logic empty heap constraint
    *
    * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   *   - `Solver::mkTerm(Kind kind) const`
    */
   SEP_EMP,
   /**
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 68499ad0d..982063b6e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1756,16 +1756,7 @@ termAtomic[cvc5::api::Term& atomTerm]
   // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity
   // as a 32-bit floating-point constant)
   | LPAREN_TOK INDEX_TOK
-    ( EMP_TOK
-      sortSymbol[type,CHECK_DECLARED]
-      sortSymbol[type2,CHECK_DECLARED]
-      {
-        // Empty heap constant in seperation logic
-        api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
-        api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2");
-        atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
-      }
-    | CHAR_TOK HEX_LITERAL 
+    ( CHAR_TOK HEX_LITERAL
       {
         std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
         atomTerm = PARSER_STATE->mkCharConstant(hexStr);
@@ -2321,7 +2312,6 @@ ATTRIBUTE_QUANTIFIER_ID_TOK : ':qid';
 EXISTS_TOK        : 'exists';
 FORALL_TOK        : 'forall';
 
-EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
 CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple';
 TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_select';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index fc75ac552..0daddea40 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -676,6 +676,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     // the Boolean sort is a placeholder here since we don't have type info
     // without type annotation
     defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
+    defineVar("sep.emp", d_solver->mkTerm(api::SEP_EMP));
 
     addSepOperators();
   }
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index 37bf0fd8b..dd85bec69 100644
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -22,9 +22,11 @@
 #include "expr/node.h"
 #include "expr/skolem_manager.h"
 #include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_engine.h"
 
 namespace cvc5 {
 namespace preprocessing {
@@ -35,9 +37,11 @@ using namespace cvc5::theory;
 
 namespace {
 
-Node preSkolemEmp(Node n,
-                         bool pol,
-                         std::map<bool, std::map<Node, Node>>& visited)
+Node preSkolemEmp(TypeNode locType,
+                  TypeNode dataType,
+                  Node n,
+                  bool pol,
+                  std::map<bool, std::map<Node, Node>>& visited)
 {
   std::map<Node, Node>::iterator it = visited[pol].find(n);
   if (it == visited[pol].end())
@@ -51,11 +55,10 @@ Node preSkolemEmp(Node n,
     {
       if (!pol)
       {
-        TypeNode tnx = n[0].getType();
-        TypeNode tny = n[1].getType();
         Node x =
-            sm->mkDummySkolem("ex", tnx, "skolem location for negated emp");
-        Node y = sm->mkDummySkolem("ey", tny, "skolem data for negated emp");
+            sm->mkDummySkolem("ex", locType, "skolem location for negated emp");
+        Node y =
+            sm->mkDummySkolem("ey", dataType, "skolem data for negated emp");
         return nm
             ->mkNode(kind::SEP_STAR,
                      nm->mkNode(kind::SEP_PTO, x, y),
@@ -78,7 +81,7 @@ Node preSkolemEmp(Node n,
         Node nc = n[i];
         if (newHasPol)
         {
-          nc = preSkolemEmp(n[i], newPol, visited);
+          nc = preSkolemEmp(locType, dataType, n[i], newPol, visited);
           childChanged = childChanged || nc != n[i];
         }
         children.push_back(nc);
@@ -105,12 +108,20 @@ SepSkolemEmp::SepSkolemEmp(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult SepSkolemEmp::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
+  TypeNode locType, dataType;
+  if (!d_preprocContext->getTheoryEngine()->getSepHeapTypes(locType, dataType))
+  {
+    Warning() << "SepSkolemEmp::applyInternal: failed to get separation logic "
+                 "heap types during preprocessing"
+              << std::endl;
+    return PreprocessingPassResult::NO_CONFLICT;
+  }
   std::map<bool, std::map<Node, Node>> visited;
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
   {
     Node prev = (*assertionsToPreprocess)[i];
     bool pol = true;
-    Node next = preSkolemEmp(prev, pol, visited);
+    Node next = preSkolemEmp(locType, dataType, prev, pol, visited);
     if (next != prev)
     {
       assertionsToPreprocess->replace(i, rewrite(next));
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds
index 17dfed893..598bec636 100644
--- a/src/theory/sep/kinds
+++ b/src/theory/sep/kinds
@@ -14,7 +14,7 @@ rewriter ::cvc5::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.
 
 nullaryoperator SEP_NIL "separation nil"
 
-operator SEP_EMP 2 "separation empty heap"
+nullaryoperator SEP_EMP "separation logic empty heap constraint"
 operator SEP_PTO 2 "points to relation"
 operator SEP_STAR 2: "separation star"
 operator SEP_WAND 2 "separation magic wand"
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index dc72783c0..bcf5c78f7 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -78,8 +78,14 @@ void TheorySep::declareSepHeap(TypeNode locT, TypeNode dataT)
     ss << d_type_ref << " -> " << d_type_data;
     throw LogicException(ss.str());
   }
-  Node nullAtom;
-  registerRefDataTypes(locT, dataT, nullAtom);
+  // otherwise set it
+  Trace("sep-type") << "Sep: assume location type " << locT
+                    << " is associated with data type " << dataT << std::endl;
+  d_loc_to_data_type[locT] = dataT;
+  // for now, we only allow heap constraints of one type
+  d_type_ref = locT;
+  d_type_data = dataT;
+  d_bound_kind[locT] = bound_default;
 }
 
 TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
@@ -107,7 +113,7 @@ void TheorySep::preRegisterTerm(TNode n)
   Kind k = n.getKind();
   if (k == SEP_PTO || k == SEP_EMP || k == SEP_STAR || k == SEP_WAND)
   {
-    registerRefDataTypesAtom(n);
+    ensureHeapTypesFor(n);
   }
 }
 
@@ -175,6 +181,7 @@ void TheorySep::computeCareGraph() {
 void TheorySep::postProcessModel( TheoryModel* m ){
   Trace("sep-model") << "Printing model for TheorySep..." << std::endl;
 
+  NodeManager* nm = NodeManager::currentNM();
   std::vector< Node > sep_children;
   Node m_neq;
   Node m_heap;
@@ -228,17 +235,18 @@ void TheorySep::postProcessModel( TheoryModel* m ){
     }
     Node nil = getNilRef( it->first );
     Node vnil = d_valuation.getModel()->getRepresentative( nil );
-    m_neq = NodeManager::currentNM()->mkNode( kind::EQUAL, nil, vnil );
+    m_neq = nm->mkNode(kind::EQUAL, nil, vnil);
     Trace("sep-model") << "sep.nil = " << vnil << std::endl;
     Trace("sep-model") << std::endl;
     if( sep_children.empty() ){
       TypeEnumerator te_domain( it->first );
       TypeEnumerator te_range( d_loc_to_data_type[it->first] );
-      m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain, *te_range );
+      TypeNode boolType = nm->booleanType();
+      m_heap = nm->mkNullaryOperator(boolType, kind::SEP_EMP);
     }else if( sep_children.size()==1 ){
       m_heap = sep_children[0];
     }else{
-      m_heap = NodeManager::currentNM()->mkNode( kind::SEP_STAR, sep_children );
+      m_heap = nm->mkNode(kind::SEP_STAR, sep_children);
     }
     m->setHeapModel( m_heap, m_neq );
   }
@@ -317,7 +325,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
     Trace("sep-lemma-debug")
         << "Reducing unlabelled assertion " << atom << std::endl;
     // introduce top-level label, add iff
-    TypeNode refType = getReferenceType(satom);
+    TypeNode refType = getReferenceType();
     Trace("sep-lemma-debug")
         << "...reference type is : " << refType << std::endl;
     Node b_lbl = getBaseLabel(refType);
@@ -350,7 +358,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
     {
       std::vector<Node> children;
       std::vector<Node> c_lems;
-      TypeNode tn = getReferenceType(satom);
+      TypeNode tn = getReferenceType();
       if (d_reference_bound_max.find(tn) != d_reference_bound_max.end())
       {
         c_lems.push_back(nm->mkNode(SUBSET, slbl, d_reference_bound_max[tn]));
@@ -433,8 +441,8 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
       }
       else
       {
-        Node kl = sm->mkDummySkolem("loc", getReferenceType(satom));
-        Node kd = sm->mkDummySkolem("data", getDataType(satom));
+        Node kl = sm->mkDummySkolem("loc", getReferenceType());
+        Node kd = sm->mkDummySkolem("data", getDataType());
         Node econc = nm->mkNode(
             SEP_LABEL,
             nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, kl, kd), d_true),
@@ -718,7 +726,7 @@ void TheorySep::postCheck(Effort level)
         continue;
       }
       needAddLemma = true;
-      TypeNode tn = getReferenceType(satom);
+      TypeNode tn = getReferenceType();
       tn = nm->mkSetType(tn);
       // tn = nm->mkSetType(nm->mkRefType(tn));
       Node o_b_lbl_mval = d_label_model[slbl].getValue(tn);
@@ -933,12 +941,14 @@ TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) {
 }
 
 //for now, assume all constraints are for the same heap type (ensured by logic exceptions thrown in computeReferenceType2)
-TypeNode TheorySep::getReferenceType( Node n ) {
+TypeNode TheorySep::getReferenceType() const
+{
   Assert(!d_type_ref.isNull());
   return d_type_ref;
 }
 
-TypeNode TheorySep::getDataType( Node n ) {
+TypeNode TheorySep::getDataType() const
+{
   Assert(!d_type_data.isNull());
   return d_type_data;
 }
@@ -980,7 +990,7 @@ int TheorySep::processAssertion(
   if( it==visited[index].end() ){
     Trace("sep-pp-debug") << "process assertion : " << n << ", index = " << index << std::endl;
     if( n.getKind()==kind::SEP_EMP ){
-      registerRefDataTypesAtom(n);
+      ensureHeapTypesFor(n);
       if( hasPol && pol ){
         references[index][n].clear();
         references_strict[index][n] = true;
@@ -988,7 +998,7 @@ int TheorySep::processAssertion(
         card = 1;
       }
     }else if( n.getKind()==kind::SEP_PTO ){
-      registerRefDataTypesAtom(n);
+      ensureHeapTypesFor(n);
       if( quantifiers::TermUtil::hasBoundVarAttr( n[0] ) ){
         TypeNode tn1 = n[0].getType();
         if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){
@@ -1065,7 +1075,7 @@ int TheorySep::processAssertion(
   }
 
   if( !underSpatial && ( !references[index][n].empty() || card>0 ) ){
-    TypeNode tn = getReferenceType( n );
+    TypeNode tn = getReferenceType();
     Assert(!tn.isNull());
     // add references to overall type
     unsigned bt = d_bound_kind[tn];
@@ -1098,46 +1108,33 @@ int TheorySep::processAssertion(
   return card;
 }
 
-void TheorySep::registerRefDataTypesAtom(Node atom)
-{
-  TypeNode tn1;
-  TypeNode tn2;
-  Kind k = atom.getKind();
-  if (k == SEP_PTO || k == SEP_EMP)
-  {
-    tn1 = atom[0].getType();
-    tn2 = atom[1].getType();
-  }
-  else
-  {
-    Assert(k == SEP_STAR || k == SEP_WAND);
-  }
-  registerRefDataTypes(tn1, tn2, atom);
-}
-
-void TheorySep::registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom)
+void TheorySep::ensureHeapTypesFor(Node atom) const
 {
-  if (!d_type_ref.isNull())
+  Assert(!atom.isNull());
+  if (!d_type_ref.isNull() && !d_type_data.isNull())
   {
-    Assert(!atom.isNull());
-    // already declared, ensure compatible
-    if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref))
-        || (!tn2.isNull() && !tn2.isComparableTo(d_type_data)))
+    if (atom.getKind() == SEP_PTO)
     {
-      std::stringstream ss;
-      ss << "ERROR: the separation logic heap type has already been set to "
-         << d_type_ref << " -> " << d_type_data
-         << " but we have a constraint that uses different heap types, "
-            "offending atom is "
-         << atom << " with associated heap type " << tn1 << " -> " << tn2
-         << std::endl;
+      TypeNode tn1 = atom[0].getType();
+      TypeNode tn2 = atom[1].getType();
+      // already declared, ensure compatible
+      if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref))
+          || (!tn2.isNull() && !tn2.isComparableTo(d_type_data)))
+      {
+        std::stringstream ss;
+        ss << "ERROR: the separation logic heap type has already been set to "
+           << d_type_ref << " -> " << d_type_data
+           << " but we have a constraint that uses different heap types, "
+              "offending atom is "
+           << atom << " with associated heap type " << tn1 << " -> " << tn2
+           << std::endl;
+      }
     }
-    return;
   }
-  // if not declared yet, and we have a separation logic constraint, throw
-  // an error.
-  if (!atom.isNull())
+  else
   {
+    // if not declared yet, and we have a separation logic constraint, throw
+    // an error.
     std::stringstream ss;
     // error, heap not declared
     ss << "ERROR: the type of the separation logic heap has not been declared "
@@ -1146,14 +1143,6 @@ void TheorySep::registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom)
        << atom << std::endl;
     throw LogicException(ss.str());
   }
-  // otherwise set it
-  Trace("sep-type") << "Sep: assume location type " << tn1
-                    << " is associated with data type " << tn2 << std::endl;
-  d_loc_to_data_type[tn1] = tn2;
-  // for now, we only allow heap constraints of one type
-  d_type_ref = tn1;
-  d_type_data = tn2;
-  d_bound_kind[tn1] = bound_default;
 }
 
 void TheorySep::initializeBounds() {
@@ -1314,7 +1303,7 @@ Node TheorySep::getLabel( Node atom, int child, Node lbl ) {
   if( it==d_label_map[atom][lbl].end() ){
     NodeManager* nm = NodeManager::currentNM();
     SkolemManager* sm = nm->getSkolemManager();
-    TypeNode refType = getReferenceType( atom );
+    TypeNode refType = getReferenceType();
     std::stringstream ss;
     ss << "__Lc" << child;
     TypeNode ltn = NodeManager::currentNM()->mkSetType(refType);
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 985513fd8..b4439c104 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -284,14 +284,14 @@ class TheorySep : public Theory {
   std::map< Node, HeapAssertInfo * > d_eqc_info;
   HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
 
-  //get global reference/data type
-  TypeNode getReferenceType( Node n );
-  TypeNode getDataType( Node n );
   /**
-   * Register reference data types for atom. Calls the method below for
-   * the appropriate types.
+   * Ensure that reference and data types have been set to something that is
+   * non-null, and compatible with separation logic constraint atom.
    */
-  void registerRefDataTypesAtom(Node atom);
+  void ensureHeapTypesFor(Node atom) const;
+  // get global reference/data type
+  TypeNode getReferenceType() const;
+  TypeNode getDataType() const;
   /**
    * This is called either when:
    * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or
diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2
index 45dd29459..5191ecd5b 100644
--- a/test/regress/regress0/sep/dispose-1.smt2
+++ b/test/regress/regress0/sep/dispose-1.smt2
@@ -13,7 +13,7 @@
 ;-----------------
 
 (assert (pto w (as sep.nil Int)))
-(assert (not (and (sep (and (_ emp Int Int) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
+(assert (not (and (sep (and sep.emp (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
 
 (check-sat)
 ;(get-model)
diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2
index 5682a0a02..3f792a4fb 100644
--- a/test/regress/regress0/sep/dup-nemp.smt2
+++ b/test/regress/regress0/sep/dup-nemp.smt2
@@ -3,6 +3,6 @@
 (declare-sort Loc 0)
 (declare-const l Loc)
 (declare-heap (Loc Loc))
-(assert (sep (not (_ emp Loc Loc)) (not (_ emp Loc Loc))))
+(assert (sep (not sep.emp) (not sep.emp)))
 (assert (pto l l))
 (check-sat)
diff --git a/test/regress/regress0/sep/issue3720-check-model.smt2 b/test/regress/regress0/sep/issue3720-check-model.smt2
index 7e9c73cb8..488c558b0 100644
--- a/test/regress/regress0/sep/issue3720-check-model.smt2
+++ b/test/regress/regress0/sep/issue3720-check-model.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --quiet
+; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic ALL)
 (declare-heap (Int Int))
-(assert (_ emp Int Int))
+(assert sep.emp)
 (check-sat)
diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index 583457e48..2d35a43d8 100644
--- a/test/regress/regress0/sep/nemp.smt2
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic QF_SEP_LIA)
 (declare-heap (Int Int))
-(assert (not (_ emp Int Int)))
+(assert (not sep.emp))
 (check-sat)
diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
index 312c97542..c83e98b66 100644
--- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
+++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
@@ -8,6 +8,6 @@
 (declare-fun a () U)
 (declare-fun b () U)
 
-(assert (_ emp U U))
+(assert sep.emp)
 (assert (sep (pto x a) (pto y b)))
 (check-sat)
diff --git a/test/regress/regress0/sep/skolem_emp.smt2 b/test/regress/regress0/sep/skolem_emp.smt2
index 2a836bef9..1c690cc75 100644
--- a/test/regress/regress0/sep/skolem_emp.smt2
+++ b/test/regress/regress0/sep/skolem_emp.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic QF_ALL)
 (declare-heap (Int Int))
-(assert (not (_ emp Int Int)))
+(assert (not sep.emp))
 (check-sat)
diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2
index 2c742c60f..31c85d62d 100644
--- a/test/regress/regress0/sep/trees-1.smt2
+++ b/test/regress/regress0/sep/trees-1.smt2
@@ -18,7 +18,7 @@
 (declare-const r Loc)
 
 (define-fun ten-tree0 ((x Loc) (d Int)) Bool 
-(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (_ emp Loc Node) (= l (as sep.nil Loc))) (and (_ emp Loc Node) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
+(or (and sep.emp (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and sep.emp (= l (as sep.nil Loc))) (and sep.emp (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
 
 (declare-const dy Int)
 (declare-const y Loc)
@@ -26,7 +26,7 @@
 (declare-const z Loc)
 
 (define-fun ord-tree0 ((x Loc) (d Int)) Bool 
-(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (_ emp Loc Node) (= y (as sep.nil Loc))) (and (_ emp Loc Node) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
+(or (and sep.emp (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and sep.emp (= y (as sep.nil Loc))) (and sep.emp (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
 
 ;------- f -------
 (assert (= y (as sep.nil Loc)))
diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2
index 02511bbae..d84d900f3 100644
--- a/test/regress/regress0/sep/wand-crash.smt2
+++ b/test/regress/regress0/sep/wand-crash.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic QF_ALL)
 (declare-heap (Int Int))
-(assert (wand (_ emp Int Int) (_ emp Int Int)))
+(assert (wand sep.emp sep.emp))
 (check-sat)
diff --git a/test/regress/regress1/sep/emp2-quant-unsat.smt2 b/test/regress/regress1/sep/emp2-quant-unsat.smt2
index cdca1a909..acdd5f6c6 100644
--- a/test/regress/regress1/sep/emp2-quant-unsat.smt2
+++ b/test/regress/regress1/sep/emp2-quant-unsat.smt2
@@ -6,7 +6,7 @@
 (declare-fun u () U)
 (declare-heap (U U))
 
-(assert (sep (not (_ emp U U)) (not (_ emp U U))))
+(assert (sep (not sep.emp) (not sep.emp)))
 
 (assert (forall ((x U) (y U)) (= x y)))
 
diff --git a/test/regress/regress1/sep/finite-witness-sat.smt2 b/test/regress/regress1/sep/finite-witness-sat.smt2
index 479dbe2b2..1d5488296 100644
--- a/test/regress/regress1/sep/finite-witness-sat.smt2
+++ b/test/regress/regress1/sep/finite-witness-sat.smt2
@@ -5,7 +5,7 @@
 (declare-const l Loc)
 (declare-heap (Loc Loc))
 
-(assert (not (_ emp Loc Loc)))
+(assert (not sep.emp))
 (assert (forall ((x Loc) (y Loc)) (not (pto x y))))
 
 
diff --git a/test/regress/regress1/sep/fmf-nemp-2.smt2 b/test/regress/regress1/sep/fmf-nemp-2.smt2
index e6e2aca98..c40106c48 100644
--- a/test/regress/regress1/sep/fmf-nemp-2.smt2
+++ b/test/regress/regress1/sep/fmf-nemp-2.smt2
@@ -6,6 +6,6 @@
 (declare-fun u1 () U)
 (declare-fun u2 () U)
 (assert (not (= u1 u2)))
-(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (_ emp U Int)) (pto x 0)))))
+(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not sep.emp) (pto x 0)))))
 ; satisfiable with heap of size 2, model of U of size 3
 (check-sat)
diff --git a/test/regress/regress1/sep/quant_wand.smt2 b/test/regress/regress1/sep/quant_wand.smt2
index 87f0a974b..63dcebfda 100644
--- a/test/regress/regress1/sep/quant_wand.smt2
+++ b/test/regress/regress1/sep/quant_wand.smt2
@@ -6,7 +6,7 @@
 
 (declare-const u Int)
 
-(assert (_ emp Int Int))
+(assert sep.emp)
 
 (assert 
 (forall ((y Int)) 
diff --git a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
index c6fa301f0..7935ccdc1 100644
--- a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
+++ b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
@@ -11,7 +11,7 @@
 (declare-const c Int)
 
 (assert (and
-        (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (_ emp Int Int)) ))
+        (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not sep.emp) ))
         (sep (pto x a) (pto y b))
   )
 )
diff --git a/test/regress/regress1/sep/wand-0526-sat.smt2 b/test/regress/regress1/sep/wand-0526-sat.smt2
index a07d0b8ae..334908e64 100644
--- a/test/regress/regress1/sep/wand-0526-sat.smt2
+++ b/test/regress/regress1/sep/wand-0526-sat.smt2
@@ -7,5 +7,5 @@
 (declare-fun u () Int)
 (declare-fun v () Int)
 (assert (wand (pto x u) (pto y v)))
-(assert (_ emp Int Int))
+(assert sep.emp)
 (check-sat)
diff --git a/test/regress/regress1/sep/wand-nterm-simp.smt2 b/test/regress/regress1/sep/wand-nterm-simp.smt2
index 47d39eb0b..4239a415e 100644
--- a/test/regress/regress1/sep/wand-nterm-simp.smt2
+++ b/test/regress/regress1/sep/wand-nterm-simp.smt2
@@ -3,6 +3,6 @@
 (set-logic QF_ALL)
 (declare-heap (Int Int))
 (declare-fun x () Int)
-(assert (wand (_ emp Int Int) (pto x 3)))
+(assert (wand sep.emp (pto x 3)))
 (check-sat)
 
diff --git a/test/regress/regress1/sep/wand-nterm-simp2.smt2 b/test/regress/regress1/sep/wand-nterm-simp2.smt2
index 647421665..15362f227 100644
--- a/test/regress/regress1/sep/wand-nterm-simp2.smt2
+++ b/test/regress/regress1/sep/wand-nterm-simp2.smt2
@@ -4,5 +4,5 @@
 (set-info :status sat)
 (declare-heap (Int Int))
 (declare-fun x () Int)
-(assert (wand (pto x 1) (_ emp Int Int)))
+(assert (wand (pto x 1) sep.emp))
 (check-sat)
diff --git a/test/regress/regress1/sep/wand-simp-unsat.smt2 b/test/regress/regress1/sep/wand-simp-unsat.smt2
index 2e90dfb26..b974b9a32 100644
--- a/test/regress/regress1/sep/wand-simp-unsat.smt2
+++ b/test/regress/regress1/sep/wand-simp-unsat.smt2
@@ -4,5 +4,5 @@
 (declare-fun x () Int)
 (declare-heap (Int Int))
 (assert (wand (pto x 1) (pto x 3)))
-(assert (_ emp Int Int))
+(assert sep.emp)
 (check-sat)