From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 8 Nov 2016 16:09:53 +0000 (-0600)
Subject: Add a few options to separation logic and sets. Minor changes to separation logic... 
X-Git-Tag: cvc5-1.0.0~5995
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa;p=cvc5.git

Add a few options to separation logic and sets. Minor changes to separation logic, change syntax for empty heap constraint.
---

diff --git a/src/options/sep_options b/src/options/sep_options
index fecf4401e..ba10cdefb 100644
--- a/src/options/sep_options
+++ b/src/options/sep_options
@@ -15,4 +15,10 @@ option sepMinimalRefine --sep-min-refine bool :default false
 option sepDisequalC --sep-deq-c bool :default true
  assume cardinality elements are distinct
 
+option sepPreSkolemEmp --sep-pre-skolem-emp bool :default false
+ eliminate emp constraint at preprocess time
+ 
+option sepChildRefine --sep-child-refine bool :default false
+ child-specific refinements of negated star, positive wand
+ 
 endmodule
diff --git a/src/options/sets_options b/src/options/sets_options
index 4c019c039..52a8f78ba 100644
--- a/src/options/sets_options
+++ b/src/options/sets_options
@@ -5,22 +5,8 @@
 
 module SETS "options/sets_options.h" Sets
 
-option setsPropagate --sets-propagate bool :default true
- determines whether to propagate learnt facts to Theory Engine / SAT solver
-
-option setsEagerLemmas --sets-eager-lemmas bool :default true
- add lemmas even at regular effort
-
-expert-option setsCare1 --sets-care1 bool :default false
- generate one lemma at a time for care graph
-
-option setsPropFull --sets-prop-full bool :default true
- additional propagation at full effort
-
-option setsGuessEmpty --sets-guess-empty int :default 0
- when to guess leaf nodes being empty (0...2 : most aggressive..least aggressive)
-
-option setsSlowLemmas --sets-slow-lemmas bool :default true
+option setsProxyLemmas --sets-proxy-lemmas bool :default false
+ introduce proxy variables eagerly to shorten lemmas
 
 option setsInferAsLemmas --sets-infer-as-lemmas bool :default true
  send inferences as lemmas
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 46469fb0d..d726b836f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -102,6 +102,7 @@
 #include "util/hash.h"
 #include "util/proof.h"
 #include "util/resource_manager.h"
+#include "options/sep_options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -3963,6 +3964,17 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-bv-to-bool", d_assertions);
     Trace("smt") << "POST bvToBool" << endl;
   }
+  if(options::sepPreSkolemEmp()) {
+    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      Node prev = d_assertions[i];
+      Node next = sep::TheorySepRewriter::preprocess( prev );
+      if( next!=prev ){
+        d_assertions.replace( i, Rewriter::rewrite( next ) );
+        Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
+        Trace("sep-preprocess") << "   ...got " << d_assertions[i] << endl;
+      }
+    }
+  }
   if( d_smt.d_logic.isQuantified() ){
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;
     
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 9c09371c4..1a0faa021 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -231,7 +231,7 @@ int ModelEngine::checkModel(){
 }
 
 bool ModelEngine::considerQuantifiedFormula( Node q ) {
-  if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ //!d_quantEngine->getModel()->isQuantifierActive( q );
+  if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) || !d_quantEngine->getModel()->isQuantifierActive( q ) ){
     return false;
   }else{
     if( options::fmfEmptySorts() ){
@@ -328,7 +328,7 @@ void ModelEngine::debugPrint( const char* c ){
   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     Trace( c ) << "   ";
-    if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){
+    if( !considerQuantifiedFormula( q ) ){
       Trace( c ) << "*Inactive* ";
     }else{
       Trace( c ) << "           ";
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds
index 6c4ad33db..318442ba5 100644
--- a/src/theory/sep/kinds
+++ b/src/theory/sep/kinds
@@ -21,7 +21,7 @@ constant SEP_NIL_REF \
 
 variable SEP_NIL "separation nil"
 
-operator SEP_EMP 1 "separation empty heap"
+operator SEP_EMP 2 "separation empty heap"
 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 e2cd4f9dc..680bd8536 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -265,7 +265,8 @@ void TheorySep::postProcessModel( TheoryModel* m ){
     Trace("sep-model") << std::endl;
     if( sep_children.empty() ){
       TypeEnumerator te_domain( it->first );
-      m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain );
+      TypeEnumerator te_range( d_loc_to_data_type[it->first] );
+      m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain, *te_range );
     }else if( sep_children.size()==1 ){
       m_heap = sep_children[0];
     }else{
@@ -311,6 +312,7 @@ void TheorySep::check(Effort e) {
 
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
+    /*
     if( atom.getKind()==kind::SEP_EMP ){
       TypeNode tn = atom[0].getType();
       if( d_emp_arg.find( tn )==d_emp_arg.end() ){
@@ -319,6 +321,7 @@ void TheorySep::check(Effort e) {
         //normalize argument TODO
       }
     }
+    */
     TNode s_atom = atom.getKind()==kind::SEP_LABEL ? atom[0] : atom;
     TNode s_lbl = atom.getKind()==kind::SEP_LABEL ? atom[1] : TNode::null();
     bool is_spatial = s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_EMP;
@@ -410,7 +413,6 @@ void TheorySep::check(Effort e) {
               //Node ssn = NodeManager::currentNM()->mkNode( kind::EQUAL, s_atom[0], getNilRef(s_atom[0].getType()) ).negate();
               //conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn );
               
-              /* TODO?
             }else if( s_atom.getKind()==kind::SEP_EMP ){
               //conc = s_lbl.eqNode( NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())) );
               Node lem;
@@ -427,7 +429,7 @@ void TheorySep::check(Effort e) {
               }
               Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl;
               d_out->lemma( lem );
-              */
+
             }else{
               //labeled emp should be rewritten
               Assert( false );
@@ -546,6 +548,12 @@ void TheorySep::check(Effort e) {
           if( d_pto_model.find( vv )==d_pto_model.end() ){
             Trace("sep-process") << "Pto : " << s_atom[0] << " (" << vv << ") -> " << s_atom[1] << std::endl;
             d_pto_model[vv] = s_atom[1];
+            
+            //replace this on pto-model since this term is more relevant
+            TypeNode vtn = vv.getType();
+            if( std::find( d_type_references_all[vtn].begin(), d_type_references_all[vtn].end(), s_atom[0] )!=d_type_references_all[vtn].end() ){
+              d_tmodel[vv] = s_atom[0];
+            }
           }
         }
       }else{
@@ -991,7 +999,7 @@ TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node
       return tn1;
     }else if( n.getKind()==kind::SEP_EMP ){
       TypeNode tn = n[0].getType();
-      TypeNode tnd;
+      TypeNode tnd = n[1].getType();
       registerRefDataTypes( tn, tnd, atom );
       card = 1;
       visited[n] = card;
@@ -1110,6 +1118,8 @@ void TheorySep::initializeBounds() {
         //must include at least one constant
         n_emp = 1;
       }
+      Trace("sep-bound") << "Card maximums : " << d_card_max[tn] << " " << d_card_max[TypeNode::null()] << std::endl;
+      Trace("sep-bound") << "Type reference size : " << d_type_references[tn].size() << std::endl;
       Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." << std::endl;
       for( unsigned r=0; r<n_emp; r++ ){
         Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
@@ -1321,6 +1331,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
         std::vector< Node > children;
         children.resize( n.getNumChildren() );
         Assert( d_label_map[n].find( lbl )!=d_label_map[n].end() );
+        std::map< int, Node > mvals;
         for( std::map< int, Node >::iterator itl = d_label_map[n][lbl].begin(); itl != d_label_map[n][lbl].end(); ++itl ){
           Node sub_lbl = itl->second;
           int sub_index = itl->first;
@@ -1339,6 +1350,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
             lbl_mval = d_label_model[sub_lbl].getValue( rtn );
           }
           Trace("sep-inst-debug") << "Sublabel value is " << lbl_mval  << std::endl;
+          mvals[sub_index] = lbl_mval;
           children[sub_index] = instantiateLabel( n[sub_index], o_lbl, sub_lbl, lbl_mval, visited, pto_model, rtn, active_lbl, ind+1 );
           if( children[sub_index].isNull() ){
             return Node::null();
@@ -1346,14 +1358,18 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
         }
         Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn.toType()));
         if( n.getKind()==kind::SEP_STAR ){
+
           //disjoint contraints
+          std::vector< Node > conj;
+          std::vector< Node > bchildren;
+          bchildren.insert( bchildren.end(), children.begin(), children.end() );
           Node vsu;
           std::vector< Node > vs;
           for( std::map< int, Node >::iterator itl = d_label_map[n][lbl].begin(); itl != d_label_map[n][lbl].end(); ++itl ){
             Node sub_lbl = itl->second;
             Node lbl_mval = d_label_model[sub_lbl].getValue( rtn );
             for( unsigned j=0; j<vs.size(); j++ ){
-              children.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval, vs[j] ).eqNode( empSet ) );
+              bchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval, vs[j] ).eqNode( empSet ) );
             }
             vs.push_back( lbl_mval );
             if( vsu.isNull() ){
@@ -1362,11 +1378,32 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
               vsu = NodeManager::currentNM()->mkNode( kind::UNION, vsu, lbl_mval );
             }
           }
-          children.push_back( vsu.eqNode( lbl ) );
+          bchildren.push_back( vsu.eqNode( lbl ) );
           
-          //return the lemma
-          Assert( children.size()>1 );
-          return NodeManager::currentNM()->mkNode( kind::AND, children );      
+          Assert( bchildren.size()>1 );
+          conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, bchildren ) );
+
+          if( options::sepChildRefine() ){
+            //child-specific refinements (TODO: use ?)
+            for( unsigned i=0; i<children.size(); i++ ){
+              std::vector< Node > tchildren;
+              Node mval = mvals[i];
+              tchildren.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, mval, lbl ) );            
+              tchildren.push_back( children[i] );
+              std::vector< Node > rem_children;
+              for( unsigned j=0; j<children.size(); j++ ){
+                if( j!=i ){
+                  rem_children.push_back( n[j] );
+                }
+              }
+              std::map< Node, Node > rvisited;
+              Node rem = rem_children.size()==1 ? rem_children[0] : NodeManager::currentNM()->mkNode( kind::SEP_STAR, rem_children );
+              rem = applyLabel( rem, NodeManager::currentNM()->mkNode( kind::SETMINUS, lbl, mval ), rvisited );
+              tchildren.push_back( rem );
+              conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, tchildren ) );
+            }
+          }
+          return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::OR, conj );
         }else{
           std::vector< Node > wchildren;
           //disjoint constraints
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 3e74bd61e..48523cd06 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -17,6 +17,8 @@
 
 #include "expr/attribute.h"
 #include "theory/sep/theory_sep_rewriter.h"
+#include "theory/quantifiers/quant_util.h"
+#include "options/sep_options.h"
 
 namespace CVC4 {
 namespace theory {
@@ -160,18 +162,57 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
   return RewriteResponse(node==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
 
-
-/*
-RewriteResponse TheorySepRewriter::preRewrite(TNode node) {
-  if( node.getKind()==kind::SEP_EMP ){
-    Trace("sep-prerewrite") << "Sep::preRewrite emp star " << std::endl;
-    return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkNode( kind::SEP_EMP, NodeManager::currentNM()->mkConst( true ) ) );
+Node TheorySepRewriter::preSkolemEmp( 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() ){
+    Trace("ajr-temp") << "Pre-skolem emp " << n << " with pol " << pol << std::endl;
+    Node ret = n;
+    if( n.getKind()==kind::SEP_EMP ){
+      if( !pol ){
+        TypeNode tnx = n[0].getType();
+        TypeNode tny = n[1].getType();
+        Node x = NodeManager::currentNM()->mkSkolem( "ex", tnx, "skolem location for negated emp" );
+        Node y = NodeManager::currentNM()->mkSkolem( "ey", tny, "skolem data for negated emp" );
+        return NodeManager::currentNM()->mkNode( kind::SEP_STAR, 
+                 NodeManager::currentNM()->mkNode( kind::SEP_PTO, x, y ),
+                 NodeManager::currentNM()->mkConst( true ) ).negate();
+      }
+    }else if( n.getKind()!=kind::FORALL && n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      bool childChanged = false;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( n.getOperator() );
+      }
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        bool newPol, newHasPol;
+        QuantPhaseReq::getPolarity( n, i, true, pol, newHasPol, newPol );
+        Node nc = n[i];
+        if( newHasPol ){
+          nc = preSkolemEmp( n[i], newPol, visited );
+          childChanged = childChanged || nc!=n[i];
+        }
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        return NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }
+    visited[pol][n] = ret;
+    return n;
   }else{
-    Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl;
-    return RewriteResponse(REWRITE_DONE, node);
+    return it->second;
+  }
+}
+
+Node TheorySepRewriter::preprocess( Node n ) {
+  if( options::sepPreSkolemEmp() ){
+    bool pol = true;
+    std::map< bool, std::map< Node, Node > > visited;
+    n = preSkolemEmp( n, pol, visited );
   }
+  return n;
 }
-*/
+
 
 }/* CVC4::theory::sep namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h
index 02adbebe5..58b79c7fd 100644
--- a/src/theory/sep/theory_sep_rewriter.h
+++ b/src/theory/sep/theory_sep_rewriter.h
@@ -43,7 +43,10 @@ public:
 
   static inline void init() {}
   static inline void shutdown() {}
-
+private:
+  static Node preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited );
+public:
+  static Node preprocess( Node n );
 };/* class TheorySepRewriter */
 
 }/* CVC4::theory::sep namespace */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index edf250c4d..51e3fe703 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -262,11 +262,11 @@ bool TheorySetsPrivate::isEntailed( Node n, bool polarity ) {
     bool conj = (n.getKind()==kind::AND)==polarity;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       bool isEnt = isEntailed( n[i], polarity );
-      if( isEnt==conj ){
-        return conj;
+      if( isEnt!=conj ){
+        return !conj;
       }
     }
-    return !conj;
+    return conj;
   }else if( n.isConst() ){
     return ( polarity && n==d_true ) || ( !polarity && n==d_false );
   }
@@ -609,36 +609,30 @@ void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) {
             Assert( d_equalityEngine.areEqual( mem[1], eq_set ) );
             if( mem[1]!=eq_set ){
               Trace("sets-debug") << "Downwards closure based on " << mem << ", eq_set = " << eq_set << std::endl;
-  #if 1
-              Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
-              nmem = Rewriter::rewrite( nmem );
-              std::vector< Node > exp;
-              exp.push_back( mem );
-              exp.push_back( mem[1].eqNode( eq_set ) );
-              assertInference( nmem, exp, lemmas, "downc" );
-              if( d_conflict ){
-                return;
-              }
-  #else
-              Node k = getProxy( eq_set );
-              Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k );
-              if( ee_areEqual( mem, pmem ) ){
+              if( !options::setsProxyLemmas() ){
                 Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
                 nmem = Rewriter::rewrite( nmem );
-                d_keep.insert( nmem );
-                d_keep.insert( pmem );
-                assertFactRec( nmem, pmem, lemmas );
+                std::vector< Node > exp;
+                exp.push_back( mem );
+                exp.push_back( mem[1].eqNode( eq_set ) );
+                assertInference( nmem, exp, lemmas, "downc" );
+                if( d_conflict ){
+                  return;
+                }
               }else{
-                Trace("sets-debug") << "...infer proxy membership" << std::endl;
-                Node exp = NodeManager::currentNM()->mkNode( kind::AND, mem, mem[1].eqNode( eq_set ) );
-                d_keep.insert( pmem );
-                d_keep.insert( exp );
-                assertFactRec( pmem, exp, lemmas );
-              }
-              if( d_conflict ){
-                return;
+                //use proxy set
+                Node k = getProxy( eq_set );
+                Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k );
+                Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
+                nmem = Rewriter::rewrite( nmem );
+                std::vector< Node > exp;
+                if( ee_areEqual( mem, pmem ) ){
+                  exp.push_back( pmem );
+                }else{
+                  nmem = NodeManager::currentNM()->mkNode( kind::OR, pmem.negate(), nmem );
+                }
+                assertInference( nmem, exp, lemmas, "downc" );
               }
-  #endif
             }
           }
         }
diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2
index 3c0e7df32..3f908c3be 100644
--- a/test/regress/regress0/sep/dispose-1.smt2
+++ b/test/regress/regress0/sep/dispose-1.smt2
@@ -11,7 +11,7 @@
 ;-----------------
 
 (assert (pto w (as sep.nil Int)))
-(assert (not (and (sep (and (emp 0) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
+(assert (not (and (sep (and (emp 0 0) (= 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 98348f617..17750eaa3 100644
--- a/test/regress/regress0/sep/dup-nemp.smt2
+++ b/test/regress/regress0/sep/dup-nemp.smt2
@@ -2,6 +2,6 @@
 (set-info :status unsat)
 (declare-sort Loc 0)
 (declare-const l Loc)
-(assert (sep (not (emp l)) (not (emp l))))
+(assert (sep (not (emp l l)) (not (emp l l))))
 (assert (pto l l))
 (check-sat)
diff --git a/test/regress/regress0/sep/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2
index 52d99d8c0..e89c0fd30 100644
--- a/test/regress/regress0/sep/emp2-quant-unsat.smt2
+++ b/test/regress/regress0/sep/emp2-quant-unsat.smt2
@@ -5,7 +5,7 @@
 (declare-sort U 0)
 (declare-fun u () U)
 
-(assert (sep (not (emp u)) (not (emp u))))
+(assert (sep (not (emp u u)) (not (emp u u))))
 
 (assert (forall ((x U) (y U)) (= x y)))
 
diff --git a/test/regress/regress0/sep/finite-witness-sat.smt2 b/test/regress/regress0/sep/finite-witness-sat.smt2
index 93413d950..8aedbfd25 100644
--- a/test/regress/regress0/sep/finite-witness-sat.smt2
+++ b/test/regress/regress0/sep/finite-witness-sat.smt2
@@ -4,7 +4,7 @@
 (declare-sort Loc 0)
 (declare-const l Loc)
 
-(assert (not (emp l)))
+(assert (not (emp l l)))
 (assert (forall ((x Loc) (y Loc)) (not (pto x y))))
 
 
diff --git a/test/regress/regress0/sep/fmf-nemp-2.smt2 b/test/regress/regress0/sep/fmf-nemp-2.smt2
index 71fe96d71..679b1e363 100644
--- a/test/regress/regress0/sep/fmf-nemp-2.smt2
+++ b/test/regress/regress0/sep/fmf-nemp-2.smt2
@@ -5,6 +5,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 u1)) (pto x 0)))))
+(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (emp u1 0)) (pto x 0)))))
 ; satisfiable with heap of size 2, model of U of size 3
 (check-sat)
diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index a0766a7e0..99d7f9c91 100644
--- a/test/regress/regress0/sep/nemp.smt2
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
-(assert (not (emp 0)))
+(assert (not (emp 0 0)))
 (check-sat)
diff --git a/test/regress/regress0/sep/quant_wand.smt2 b/test/regress/regress0/sep/quant_wand.smt2
index d71b937fc..9c38fb405 100644
--- a/test/regress/regress0/sep/quant_wand.smt2
+++ b/test/regress/regress0/sep/quant_wand.smt2
@@ -5,7 +5,7 @@
 
 (declare-const u Int)
 
-(assert (emp 0))
+(assert (emp 0 0))
 
 (assert 
 (forall ((y Int)) 
diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
index 9239fb770..42efae553 100644
--- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
+++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
@@ -7,6 +7,6 @@
 (declare-fun a () U)
 (declare-fun b () U)
 
-(assert (emp x))
+(assert (emp x x))
 (assert (sep (pto x a) (pto y b)))
 (check-sat)
diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2
index 8a46d9fdd..3fa0d0555 100644
--- a/test/regress/regress0/sep/trees-1.smt2
+++ b/test/regress/regress0/sep/trees-1.smt2
@@ -6,6 +6,8 @@
 
 (declare-datatypes () ((Node (node (data Int) (left Loc) (right Loc)))))
 
+(declare-fun data0 () Node)
+
 (declare-const dv Int)
 (declare-const v Loc)
 
@@ -15,7 +17,7 @@
 (declare-const r Loc)
 
 (define-fun ten-tree0 ((x Loc) (d Int)) Bool 
-(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0) (= l (as sep.nil Loc))) (and (emp loc0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
+(or (and (emp loc0 data0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0 data0) (= l (as sep.nil Loc))) (and (emp loc0 data0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
 
 (declare-const dy Int)
 (declare-const y Loc)
@@ -23,7 +25,7 @@
 (declare-const z Loc)
 
 (define-fun ord-tree0 ((x Loc) (d Int)) Bool 
-(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0) (= y (as sep.nil Loc))) (and (emp loc0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
+(or (and (emp loc0 data0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0 data0) (= y (as sep.nil Loc))) (and (emp loc0 data0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
 
 ;------- f -------
 (assert (= y (as sep.nil Loc)))
diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2
index fa0aab591..12aa0a67e 100644
--- a/test/regress/regress0/sep/wand-0526-sat.smt2
+++ b/test/regress/regress0/sep/wand-0526-sat.smt2
@@ -6,5 +6,5 @@
 (declare-fun u () Int)
 (declare-fun v () Int)
 (assert (wand (pto x u) (pto y v)))
-(assert (emp 0))
+(assert (emp 0 0))
 (check-sat)
diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2
index 1d799c8c9..dad089f8b 100644
--- a/test/regress/regress0/sep/wand-crash.smt2
+++ b/test/regress/regress0/sep/wand-crash.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
-(assert (wand (emp 0) (emp 0)))
+(assert (wand (emp 0 0) (emp 0 0)))
 (check-sat)
diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2
index 0db7330d1..b59b53b58 100644
--- a/test/regress/regress0/sep/wand-nterm-simp.smt2
+++ b/test/regress/regress0/sep/wand-nterm-simp.smt2
@@ -2,6 +2,6 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
-(assert (wand (emp x) (pto x 3)))
+(assert (wand (emp x x) (pto x 3)))
 (check-sat)
 
diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2
index cce0f79e3..fa6a83143 100644
--- a/test/regress/regress0/sep/wand-nterm-simp2.smt2
+++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2
@@ -3,5 +3,5 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun x () Int)
-(assert (wand (pto x 1) (emp x)))
+(assert (wand (pto x 1) (emp x x)))
 (check-sat)
diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2
index c9851661a..850be7b97 100755
--- a/test/regress/regress0/sep/wand-simp-unsat.smt2
+++ b/test/regress/regress0/sep/wand-simp-unsat.smt2
@@ -3,5 +3,5 @@
 (set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (pto x 3)))
-(assert (emp x))
+(assert (emp x x))
 (check-sat)