(new theory) Update TheorySep to new interface (#4947)

This updates the theory of separation logic to the new interface, which involves splitting up its check method based on the 4 check callbacks and using the theory state in the standard way.

No behavior changes, unfortunately a lot of code had to change indentation and was updated to new coding guidelines.

1 files changed, 640 insertions, 531 deletions

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 0059d9f3a..dc8ec9203 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -34,6 +34,7 @@
 #include "theory/valuation.h"
 
 using namespace std;
+using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
@@ -50,7 +51,6 @@ TheorySep::TheorySep(context::Context* c,
       d_bounds_init(false),
       d_state(c, u, valuation),
       d_notify(*this),
-      d_conflict(c, false),
       d_reduce(u),
       d_infer(c),
       d_infer_exp(c),
@@ -115,18 +115,18 @@ bool TheorySep::propagateLit(TNode literal)
 {
   Debug("sep") << "TheorySep::propagateLit(" << literal << ")" << std::endl;
   // If already in conflict, no more propagation
-  if (d_conflict) {
+  if (d_state.isInConflict())
+  {
     Debug("sep") << "TheorySep::propagateLit(" << literal
                  << "): already in conflict" << std::endl;
     return false;
   }
   bool ok = d_out->propagate(literal);
   if (!ok) {
-    d_conflict = true;
+    d_state.notifyInConflict();
   }
   return ok;
-}/* TheorySep::propagate(TNode) */
-
+}
 
 void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
   if( literal.getKind()==kind::SEP_LABEL ||
@@ -160,29 +160,6 @@ TrustNode TheorySep::explain(TNode literal)
 // SHARING
 /////////////////////////////////////////////////////////////////////////////
 
-void TheorySep::notifySharedTerm(TNode t)
-{
-  Debug("sep") << "TheorySep::notifySharedTerm(" << t << ")" << std::endl;
-  d_equalityEngine->addTriggerTerm(t, THEORY_SEP);
-}
-
-
-EqualityStatus TheorySep::getEqualityStatus(TNode a, TNode b) {
-  Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
-  if (d_equalityEngine->areEqual(a, b))
-  {
-    // The terms are implied to be equal
-    return EQUALITY_TRUE;
-  }
-  else if (d_equalityEngine->areDisequal(a, b, false))
-  {
-    // The terms are implied to be dis-equal
-    return EQUALITY_FALSE;
-  }
-  return EQUALITY_UNKNOWN;//FALSE_IN_MODEL;
-}
-
-
 void TheorySep::computeCareGraph() {
   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
@@ -213,17 +190,6 @@ void TheorySep::computeCareGraph() {
 // MODEL GENERATION
 /////////////////////////////////////////////////////////////////////////////
 
-bool TheorySep::collectModelInfo(TheoryModel* m)
-{
-  set<Node> termSet;
-
-  // Compute terms appearing in assertions and shared terms
-  computeRelevantTerms(termSet);
-
-  // Send the equality engine information to the model
-  return m->assertEqualityEngine(d_equalityEngine, &termSet);
-}
-
 void TheorySep::postProcessModel( TheoryModel* m ){
   Trace("sep-model") << "Printing model for TheorySep..." << std::endl;
   
@@ -312,532 +278,664 @@ void TheorySep::presolve() {
 // MAIN SOLVER
 /////////////////////////////////////////////////////////////////////////////
 
-
-void TheorySep::check(Effort e) {
-  if (done() && !fullEffort(e) && e != EFFORT_LAST_CALL) {
-    return;
+bool TheorySep::preNotifyFact(
+    TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
+{
+  TNode satom = atom.getKind() == SEP_LABEL ? atom[0] : atom;
+  TNode slbl = atom.getKind() == SEP_LABEL ? atom[1] : TNode::null();
+  bool isSpatial = isSpatialKind(satom.getKind());
+  if (isSpatial)
+  {
+    reduceFact(atom, polarity, fact);
+    if (!slbl.isNull())
+    {
+      d_spatial_assertions.push_back(fact);
+    }
   }
+  // assert to equality if non-spatial or a labelled pto
+  if (!isSpatial || (!slbl.isNull() && satom.getKind() == SEP_PTO))
+  {
+    return false;
+  }
+  // otherwise, maybe propagate
+  doPendingFacts();
+  return true;
+}
 
-  getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep);
+void TheorySep::notifyFact(TNode atom,
+                           bool polarity,
+                           TNode fact,
+                           bool isInternal)
+{
+  TNode satom = atom.getKind() == SEP_LABEL ? atom[0] : atom;
+  if (atom.getKind() == SEP_LABEL && atom[0].getKind() == SEP_PTO)
+  {
+    // associate the equivalence class of the lhs with this pto
+    Node r = getRepresentative(atom[1]);
+    HeapAssertInfo* ei = getOrMakeEqcInfo(r, true);
+    addPto(ei, r, atom, polarity);
+  }
+  // maybe propagate
+  doPendingFacts();
+}
 
-  TimerStat::CodeTimer checkTimer(d_checkTime);
-  Trace("sep-check") << "Sep::check(): " << e << endl;
+void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
+{
+  if (d_reduce.find(fact) != d_reduce.end())
+  {
+    // already reduced
+    return;
+  }
+  d_reduce.insert(fact);
+  TNode satom = atom.getKind() == SEP_LABEL ? atom[0] : atom;
+  TNode slbl = atom.getKind() == SEP_LABEL ? atom[1] : TNode::null();
   NodeManager* nm = NodeManager::currentNM();
-
-  while( !done() && !d_conflict ){
-    // Get all the assertions
-    Assertion assertion = get();
-    TNode fact = assertion.d_assertion;
-
-    Trace("sep-assert") << "TheorySep::check(): processing " << fact << std::endl;
-
-    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() ){
-        d_emp_arg[tn] = atom[0];
-      }else{
-        //normalize argument TODO
-      }
+  if (slbl.isNull())
+  {
+    Trace("sep-lemma-debug")
+        << "Reducing unlabelled assertion " << atom << std::endl;
+    // introduce top-level label, add iff
+    TypeNode refType = getReferenceType(satom);
+    Trace("sep-lemma-debug")
+        << "...reference type is : " << refType << std::endl;
+    Node b_lbl = getBaseLabel(refType);
+    Node satom_new = nm->mkNode(SEP_LABEL, satom, b_lbl);
+    Node lem;
+    Trace("sep-lemma-debug") << "...polarity is " << polarity << std::endl;
+    if (polarity)
+    {
+      lem = nm->mkNode(OR, satom.negate(), satom_new);
     }
-    */
-    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;
-    if( is_spatial && s_lbl.isNull() ){
-      if( d_reduce.find( fact )==d_reduce.end() ){
-        Trace("sep-lemma-debug") << "Reducing unlabelled assertion " << atom << std::endl;
-        d_reduce.insert( fact );
-        //introduce top-level label, add iff
-        TypeNode refType = getReferenceType( s_atom );
-        Trace("sep-lemma-debug") << "...reference type is : " << refType << std::endl;
-        Node b_lbl = getBaseLabel( refType );
-        Node s_atom_new = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, s_atom, b_lbl );
-        Node lem;
-        Trace("sep-lemma-debug") << "...polarity is " << polarity << std::endl;
-        if( polarity ){
-          lem = NodeManager::currentNM()->mkNode( kind::OR, s_atom.negate(), s_atom_new );
-        }else{
-          lem = NodeManager::currentNM()->mkNode( kind::OR, s_atom, s_atom_new.negate() );
-        }
-        Trace("sep-lemma-debug") << "Sep::Lemma : base reduction : " << lem << std::endl;
-        d_out->lemma( lem );
+    else
+    {
+      lem = nm->mkNode(OR, satom, satom_new.negate());
+    }
+    Trace("sep-lemma-debug")
+        << "Sep::Lemma : base reduction : " << lem << std::endl;
+    d_out->lemma(lem);
+    return;
+  }
+  Trace("sep-lemma-debug") << "Reducing assertion " << fact << std::endl;
+  Node conc;
+  if (Node* in_map = FindOrNull(d_red_conc[slbl], satom))
+  {
+    conc = *in_map;
+  }
+  else
+  {
+    // make conclusion based on type of assertion
+    if (satom.getKind() == SEP_STAR || satom.getKind() == SEP_WAND)
+    {
+      std::vector<Node> children;
+      std::vector<Node> c_lems;
+      TypeNode tn = getReferenceType(satom);
+      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]));
       }
-    }else{
-      //do reductions
-      if( is_spatial ){
-        if( d_reduce.find( fact )==d_reduce.end() ){
-          Trace("sep-lemma-debug") << "Reducing assertion " << fact << std::endl;
-          d_reduce.insert( fact );
-          Node conc;
-          if (Node* in_map = FindOrNull(d_red_conc[s_lbl], s_atom))
-          {
-            conc = *in_map;
-          }
-          else
+      std::vector<Node> labels;
+      getLabelChildren(satom, slbl, children, labels);
+      Node empSet = nm->mkConst(EmptySet(slbl.getType()));
+      Assert(children.size() > 1);
+      if (satom.getKind() == SEP_STAR)
+      {
+        // reduction for heap : union, pairwise disjoint
+        Node ulem = nm->mkNode(UNION, labels[0], labels[1]);
+        size_t lsize = labels.size();
+        for (size_t i = 2; i < lsize; i++)
+        {
+          ulem = nm->mkNode(UNION, ulem, labels[i]);
+        }
+        ulem = slbl.eqNode(ulem);
+        Trace("sep-lemma-debug")
+            << "Sep::Lemma : star reduction, union : " << ulem << std::endl;
+        c_lems.push_back(ulem);
+        for (size_t i = 0; i < lsize; i++)
+        {
+          for (size_t j = (i + 1); j < lsize; j++)
           {
-            //make conclusion based on type of assertion
-            if( s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND ){
-              std::vector< Node > children;
-              std::vector< Node > c_lems;
-              TypeNode tn = getReferenceType( s_atom );
-              if( d_reference_bound_max.find( tn )!=d_reference_bound_max.end() ){
-                c_lems.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, s_lbl, d_reference_bound_max[tn] ) );
-              }
-              std::vector< Node > labels;
-              getLabelChildren( s_atom, s_lbl, children, labels );
-              Node empSet =
-                  NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType()));
-              Assert(children.size() > 1);
-              if( s_atom.getKind()==kind::SEP_STAR ){
-                //reduction for heap : union, pairwise disjoint
-                Node ulem = NodeManager::currentNM()->mkNode( kind::UNION, labels[0], labels[1] );
-                for( unsigned i=2; i<labels.size(); i++ ){
-                  ulem = NodeManager::currentNM()->mkNode( kind::UNION, ulem, labels[i] );
-                }
-                ulem = s_lbl.eqNode( ulem );
-                Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, union : " << ulem << std::endl;
-                c_lems.push_back( ulem );
-                for( unsigned i=0; i<labels.size(); i++ ){
-                  for( unsigned j=(i+1); j<labels.size(); j++ ){
-                    Node s = NodeManager::currentNM()->mkNode( kind::INTERSECTION, labels[i], labels[j] );
-                    Node ilem = s.eqNode( empSet );
-                    Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, disjoint : " << ilem << std::endl;
-                    c_lems.push_back( ilem );
-                  }
-                }
-              }else{
-                Node ulem = NodeManager::currentNM()->mkNode( kind::UNION, s_lbl, labels[0] );
-                ulem = ulem.eqNode( labels[1] );
-                Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, union : " << ulem << std::endl;
-                c_lems.push_back( ulem );
-                Node s = NodeManager::currentNM()->mkNode( kind::INTERSECTION, s_lbl, labels[0] );
-                Node ilem = s.eqNode( empSet );
-                Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, disjoint : " << ilem << std::endl;
-                c_lems.push_back( ilem );
-                //nil does not occur in labels[0]
-                Node nr = getNilRef( tn );
-                Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, labels[0] ).negate();
-                Trace("sep-lemma") << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem << std::endl;
-                d_out->lemma( nrlem );
-              }
-              //send out definitional lemmas for introduced sets
-              for( unsigned j=0; j<c_lems.size(); j++ ){
-                Trace("sep-lemma") << "Sep::Lemma : definition : " << c_lems[j] << std::endl;
-                d_out->lemma( c_lems[j] );
-              }
-              //children.insert( children.end(), c_lems.begin(), c_lems.end() );
-              conc = NodeManager::currentNM()->mkNode( kind::AND, children );
-            }else if( s_atom.getKind()==kind::SEP_PTO ){
-              Node ss = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] );
-              if( s_lbl!=ss ){
-                conc = s_lbl.eqNode( ss );
-              }
-              //not needed anymore: semantics of sep.nil is enforced globally
-              //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 );
-              
-            }else if( s_atom.getKind()==kind::SEP_EMP ){
-              // conc = s_lbl.eqNode(
-              // NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType())) );
-              Node lem;
-              Node emp_s =
-                  NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType()));
-              if( polarity ){
-                lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), s_lbl.eqNode( emp_s ) );
-              }else{
-                Node kl = NodeManager::currentNM()->mkSkolem( "loc", getReferenceType( s_atom ) );
-                Node kd = NodeManager::currentNM()->mkSkolem( "data", getDataType( s_atom ) );
-                Node econc = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, 
-                               NodeManager::currentNM()->mkNode( kind::SEP_STAR, NodeManager::currentNM()->mkNode( kind::SEP_PTO, kl, kd ), d_true ), s_lbl );
-                //Node econc = NodeManager::currentNM()->mkNode( kind::AND, s_lbl.eqNode( emp_s ).negate(), 
-                lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), econc );
-              }
-              Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl;
-              d_out->lemma( lem );
-
-            }else{
-              //labeled emp should be rewritten
-              Assert(false);
-            }
-            d_red_conc[s_lbl][s_atom] = conc;
-          }
-          if( !conc.isNull() ){
-            bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity;
-            if( !use_polarity ){
-              // introduce guard, assert positive version
-              Trace("sep-lemma-debug") << "Negated spatial constraint asserted to sep theory: " << fact << std::endl;
-              Node g = nm->mkSkolem("G", nm->booleanType());
-              d_neg_guard_strategy[g].reset(new DecisionStrategySingleton(
-                  "sep_neg_guard", g, getSatContext(), getValuation()));
-              DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get();
-              getDecisionManager()->registerStrategy(
-                  DecisionManager::STRAT_SEP_NEG_GUARD, ds);
-              Node lit = ds->getLiteral(0);
-              d_neg_guard[s_lbl][s_atom] = lit;
-              Trace("sep-lemma-debug") << "Neg guard : " << s_lbl << " " << s_atom << " " << lit << std::endl;
-              AlwaysAssert(!lit.isNull());
-              d_neg_guards.push_back( lit );
-              d_guard_to_assertion[lit] = s_atom;
-              //Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, lit, conc );
-              Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit.negate(), conc );
-              Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem << std::endl;
-              d_out->lemma( lem );
-            }else{
-              //reduce based on implication
-              Node lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), conc );
-              Trace("sep-lemma") << "Sep::Lemma : reduction : " << lem << std::endl;
-              d_out->lemma( lem );
-            }
-          }else{
-            Trace("sep-lemma-debug") << "Trivial conclusion, do not add lemma." << std::endl;
+            Node s = nm->mkNode(INTERSECTION, labels[i], labels[j]);
+            Node ilem = s.eqNode(empSet);
+            Trace("sep-lemma-debug")
+                << "Sep::Lemma : star reduction, disjoint : " << ilem
+                << std::endl;
+            c_lems.push_back(ilem);
           }
         }
       }
-      //assert to equality engine
-      if( !is_spatial ){
-        Trace("sep-assert") << "Asserting " << atom << ", pol = " << polarity << " to EE..." << std::endl;
-        if( s_atom.getKind()==kind::EQUAL ){
-          d_equalityEngine->assertEquality(atom, polarity, fact);
-        }else{
-          d_equalityEngine->assertPredicate(atom, polarity, fact);
-        }
-        Trace("sep-assert") << "Done asserting " << atom << " to EE." << std::endl;
-      }else if( s_atom.getKind()==kind::SEP_PTO ){
-        Node pto_lbl = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] );
-        Assert(s_lbl == pto_lbl);
-        Trace("sep-assert") << "Asserting " << s_atom << std::endl;
-        d_equalityEngine->assertPredicate(s_atom, polarity, fact);
-        //associate the equivalence class of the lhs with this pto
-        Node r = getRepresentative( s_lbl );
-        HeapAssertInfo * ei = getOrMakeEqcInfo( r, true );
-        addPto( ei, r, atom, polarity );
-      }
-      //maybe propagate
-      doPendingFacts();
-      //add to spatial assertions
-      if( !d_conflict && is_spatial ){
-        d_spatial_assertions.push_back( fact );
+      else
+      {
+        Node ulem = nm->mkNode(UNION, slbl, labels[0]);
+        ulem = ulem.eqNode(labels[1]);
+        Trace("sep-lemma-debug")
+            << "Sep::Lemma : wand reduction, union : " << ulem << std::endl;
+        c_lems.push_back(ulem);
+        Node s = nm->mkNode(INTERSECTION, slbl, labels[0]);
+        Node ilem = s.eqNode(empSet);
+        Trace("sep-lemma-debug")
+            << "Sep::Lemma : wand reduction, disjoint : " << ilem << std::endl;
+        c_lems.push_back(ilem);
+        // nil does not occur in labels[0]
+        Node nr = getNilRef(tn);
+        Node nrlem = nm->mkNode(MEMBER, nr, labels[0]).negate();
+        Trace("sep-lemma")
+            << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem
+            << std::endl;
+        d_out->lemma(nrlem);
       }
+      // send out definitional lemmas for introduced sets
+      for (const Node& clem : c_lems)
+      {
+        Trace("sep-lemma") << "Sep::Lemma : definition : " << clem << std::endl;
+        d_out->lemma(clem);
+      }
+      conc = nm->mkNode(AND, children);
+    }
+    else if (satom.getKind() == SEP_PTO)
+    {
+      Node ss = nm->mkNode(SINGLETON, satom[0]);
+      if (slbl != ss)
+      {
+        conc = slbl.eqNode(ss);
+      }
+      // note semantics of sep.nil is enforced globally
+    }
+    else if (satom.getKind() == SEP_EMP)
+    {
+      Node lem;
+      Node emp_s = nm->mkConst(EmptySet(slbl.getType()));
+      if (polarity)
+      {
+        lem = nm->mkNode(OR, fact.negate(), slbl.eqNode(emp_s));
+      }
+      else
+      {
+        Node kl = nm->mkSkolem("loc", getReferenceType(satom));
+        Node kd = nm->mkSkolem("data", getDataType(satom));
+        Node econc = nm->mkNode(
+            SEP_LABEL,
+            nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, kl, kd), d_true),
+            slbl);
+        // Node econc = nm->mkNode( AND, slbl.eqNode( emp_s ).negate(),
+        lem = nm->mkNode(OR, fact.negate(), econc);
+      }
+      Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl;
+      d_out->lemma(lem);
     }
+    else
+    {
+      // labeled emp should be rewritten
+      Unreachable();
+    }
+    d_red_conc[slbl][satom] = conc;
   }
+  if (conc.isNull())
+  {
+    Trace("sep-lemma-debug")
+        << "Trivial conclusion, do not add lemma." << std::endl;
+    return;
+  }
+  bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity;
+  if (!use_polarity)
+  {
+    // introduce guard, assert positive version
+    Trace("sep-lemma-debug")
+        << "Negated spatial constraint asserted to sep theory: " << fact
+        << std::endl;
+    Node g = nm->mkSkolem("G", nm->booleanType());
+    d_neg_guard_strategy[g].reset(new DecisionStrategySingleton(
+        "sep_neg_guard", g, getSatContext(), getValuation()));
+    DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get();
+    getDecisionManager()->registerStrategy(DecisionManager::STRAT_SEP_NEG_GUARD,
+                                           ds);
+    Node lit = ds->getLiteral(0);
+    d_neg_guard[slbl][satom] = lit;
+    Trace("sep-lemma-debug")
+        << "Neg guard : " << slbl << " " << satom << " " << lit << std::endl;
+    AlwaysAssert(!lit.isNull());
+    d_neg_guards.push_back(lit);
+    d_guard_to_assertion[lit] = satom;
+    // Node lem = nm->mkNode( EQUAL, lit, conc );
+    Node lem = nm->mkNode(OR, lit.negate(), conc);
+    Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem << std::endl;
+    d_out->lemma(lem);
+  }
+  else
+  {
+    // reduce based on implication
+    Node lem = nm->mkNode(OR, fact.negate(), conc);
+    Trace("sep-lemma") << "Sep::Lemma : reduction : " << lem << std::endl;
+    d_out->lemma(lem);
+  }
+}
 
-  if( e == EFFORT_LAST_CALL && !d_conflict && !d_valuation.needCheck() ){
-    Trace("sep-process") << "Checking heap at full effort..." << std::endl;
-    d_label_model.clear();
-    d_tmodel.clear();
-    d_pto_model.clear();
-    Trace("sep-process") << "---Locations---" << std::endl;
-    std::map< Node, int > min_id;
-    for( std::map< TypeNode, std::vector< Node > >::iterator itt = d_type_references_all.begin(); itt != d_type_references_all.end(); ++itt ){
-      for( unsigned k=0; k<itt->second.size(); k++ ){
-        Node t = itt->second[k];
-        Trace("sep-process") << "  " << t << " = ";
-        if( d_valuation.getModel()->hasTerm( t ) ){
-          Node v = d_valuation.getModel()->getRepresentative( t );
-          Trace("sep-process") << v << std::endl;
-          //take minimal id
-          std::map< Node, unsigned >::iterator itrc = d_type_ref_card_id.find( t );
-          int tid = itrc==d_type_ref_card_id.end() ? -1 : (int)itrc->second;
-          bool set_term_model;
-          if( d_tmodel.find( v )==d_tmodel.end() ){
-            set_term_model = true;
-          }else{
-            set_term_model = min_id[v]>tid;
-          }
-          if( set_term_model ){
-            d_tmodel[v] = t;
-            min_id[v] = tid;
-          }
+bool TheorySep::isSpatialKind(Kind k) const
+{
+  return k == SEP_STAR || k == SEP_WAND || k == SEP_PTO || k == SEP_EMP;
+}
+
+void TheorySep::postCheck(Effort level)
+{
+  if (level != EFFORT_LAST_CALL || d_state.isInConflict()
+      || d_valuation.needCheck())
+  {
+    return;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Trace("sep-process") << "Checking heap at full effort..." << std::endl;
+  d_label_model.clear();
+  d_tmodel.clear();
+  d_pto_model.clear();
+  Trace("sep-process") << "---Locations---" << std::endl;
+  std::map<Node, int> min_id;
+  for (std::map<TypeNode, std::vector<Node> >::iterator itt =
+           d_type_references_all.begin();
+       itt != d_type_references_all.end();
+       ++itt)
+  {
+    for (const Node& t : itt->second)
+    {
+      Trace("sep-process") << "  " << t << " = ";
+      if (d_valuation.getModel()->hasTerm(t))
+      {
+        Node v = d_valuation.getModel()->getRepresentative(t);
+        Trace("sep-process") << v << std::endl;
+        // take minimal id
+        std::map<Node, unsigned>::iterator itrc = d_type_ref_card_id.find(t);
+        int tid = itrc == d_type_ref_card_id.end() ? -1 : (int)itrc->second;
+        bool set_term_model;
+        if (d_tmodel.find(v) == d_tmodel.end())
+        {
+          set_term_model = true;
         }else{
-          Trace("sep-process") << "?" << std::endl;
+          set_term_model = min_id[v] > tid;
         }
+        if (set_term_model)
+        {
+          d_tmodel[v] = t;
+          min_id[v] = tid;
+        }
+      }
+      else
+      {
+        Trace("sep-process") << "?" << std::endl;
       }
     }
-    Trace("sep-process") << "---" << std::endl;
-    //build positive/negative assertion lists for labels
-    std::map< Node, bool > assert_active;
-    //get the inactive assertions
-    std::map< Node, std::vector< Node > > lbl_to_assertions;
-    for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
-      Node fact = (*i);
-      bool polarity = fact.getKind() != kind::NOT;
-      TNode atom = polarity ? fact : fact[0];
-      Assert(atom.getKind() == kind::SEP_LABEL);
-      TNode s_atom = atom[0];
-      TNode s_lbl = atom[1];
-      lbl_to_assertions[s_lbl].push_back( fact );
-      //check whether assertion is active : either polarity=true, or guard is not asserted false
-      assert_active[fact] = true;
-      bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity;
-      if( use_polarity ){
-        if( s_atom.getKind()==kind::SEP_PTO ){
-          Node vv = d_valuation.getModel()->getRepresentative( s_atom[0] );
-          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{
-        if( d_neg_guard[s_lbl].find( s_atom )!=d_neg_guard[s_lbl].end() ){
-          //check if the guard is asserted positively
-          Node guard = d_neg_guard[s_lbl][s_atom];
-          bool value;
-          if( getValuation().hasSatValue( guard, value ) ) {
-            assert_active[fact] = value;
+  }
+  Trace("sep-process") << "---" << std::endl;
+  // build positive/negative assertion lists for labels
+  std::map<Node, bool> assert_active;
+  // get the inactive assertions
+  std::map<Node, std::vector<Node> > lbl_to_assertions;
+  for (NodeList::const_iterator i = d_spatial_assertions.begin();
+       i != d_spatial_assertions.end();
+       ++i)
+  {
+    Node fact = (*i);
+    bool polarity = fact.getKind() != NOT;
+    TNode atom = polarity ? fact : fact[0];
+    Assert(atom.getKind() == SEP_LABEL);
+    TNode satom = atom[0];
+    TNode slbl = atom[1];
+    lbl_to_assertions[slbl].push_back(fact);
+    // check whether assertion is active : either polarity=true, or guard is not
+    // asserted false
+    assert_active[fact] = true;
+    bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity;
+    if (use_polarity)
+    {
+      if (satom.getKind() == SEP_PTO)
+      {
+        Node vv = d_valuation.getModel()->getRepresentative(satom[0]);
+        if (d_pto_model.find(vv) == d_pto_model.end())
+        {
+          Trace("sep-process") << "Pto : " << satom[0] << " (" << vv << ") -> "
+                               << satom[1] << std::endl;
+          d_pto_model[vv] = satom[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(),
+                        satom[0])
+              != d_type_references_all[vtn].end())
+          {
+            d_tmodel[vv] = satom[0];
           }
         }
       }
     }
-    //(recursively) set inactive sub-assertions
-    for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
-      Node fact = (*i);
-      if( !assert_active[fact] ){
-        setInactiveAssertionRec( fact, lbl_to_assertions, assert_active );
+    else
+    {
+      if (d_neg_guard[slbl].find(satom) != d_neg_guard[slbl].end())
+      {
+        // check if the guard is asserted positively
+        Node guard = d_neg_guard[slbl][satom];
+        bool value;
+        if (getValuation().hasSatValue(guard, value))
+        {
+          assert_active[fact] = value;
+        }
       }
     }
-    //set up model information based on active assertions
+  }
+  //(recursively) set inactive sub-assertions
+  for (NodeList::const_iterator i = d_spatial_assertions.begin();
+       i != d_spatial_assertions.end();
+       ++i)
+  {
+    Node fact = (*i);
+    if (!assert_active[fact])
+    {
+      setInactiveAssertionRec(fact, lbl_to_assertions, assert_active);
+    }
+  }
+  // set up model information based on active assertions
+  for (NodeList::const_iterator i = d_spatial_assertions.begin();
+       i != d_spatial_assertions.end();
+       ++i)
+  {
+    Node fact = (*i);
+    bool polarity = fact.getKind() != NOT;
+    TNode atom = polarity ? fact : fact[0];
+    TNode satom = atom[0];
+    TNode slbl = atom[1];
+    if (assert_active[fact])
+    {
+      computeLabelModel(slbl);
+    }
+  }
+  // debug print
+  if (Trace.isOn("sep-process"))
+  {
+    Trace("sep-process") << "--- Current spatial assertions : " << std::endl;
     for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
       Node fact = (*i);
-      bool polarity = fact.getKind() != kind::NOT;
-      TNode atom = polarity ? fact : fact[0];
-      TNode s_atom = atom[0];
-      TNode s_lbl = atom[1];
-      if( assert_active[fact] ){
-        computeLabelModel( s_lbl );
-      }
-    }
-    //debug print
-    if( Trace.isOn("sep-process") ){
-      Trace("sep-process") << "--- Current spatial assertions : " << std::endl;
-      for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
-        Node fact = (*i);
-        Trace("sep-process") << "  " << fact;
-        if( !assert_active[fact] ){
-          Trace("sep-process") << " [inactive]";
-        }
-        Trace("sep-process") << std::endl;
+      Trace("sep-process") << "  " << fact;
+      if (!assert_active[fact])
+      {
+        Trace("sep-process") << " [inactive]";
       }
-      Trace("sep-process") << "---" << std::endl;
+      Trace("sep-process") << std::endl;
     }
-    if(Trace.isOn("sep-eqc")) {
-      eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
-      Trace("sep-eqc") << "EQC:" << std::endl;
-      while( !eqcs2_i.isFinished() ){
-        Node eqc = (*eqcs2_i);
-        eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine);
-        Trace("sep-eqc") << "Eqc( " << eqc << " ) : { ";
-        while( !eqc2_i.isFinished() ) {
-          if( (*eqc2_i)!=eqc ){
-            Trace("sep-eqc") << (*eqc2_i) << " ";
-          }
-          ++eqc2_i;
+    Trace("sep-process") << "---" << std::endl;
+  }
+  if (Trace.isOn("sep-eqc"))
+  {
+    eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
+    Trace("sep-eqc") << "EQC:" << std::endl;
+    while (!eqcs2_i.isFinished())
+    {
+      Node eqc = (*eqcs2_i);
+      eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine);
+      Trace("sep-eqc") << "Eqc( " << eqc << " ) : { ";
+      while (!eqc2_i.isFinished())
+      {
+        if ((*eqc2_i) != eqc)
+        {
+          Trace("sep-eqc") << (*eqc2_i) << " ";
         }
-        Trace("sep-eqc") << " } " << std::endl;
-        ++eqcs2_i;
+        ++eqc2_i;
       }
-      Trace("sep-eqc") << std::endl;
+      Trace("sep-eqc") << " } " << std::endl;
+      ++eqcs2_i;
     }
-    
-    bool addedLemma = false;
-    bool needAddLemma = false;
-    //check negated star / positive wand
-    if( options::sepCheckNeg() ){
-      //get active labels
-      std::map< Node, bool > active_lbl;
-      if( options::sepMinimalRefine() ){
-        for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
-          Node fact = (*i);
-          bool polarity = fact.getKind() != kind::NOT;
-          TNode atom = polarity ? fact : fact[0];
-          TNode s_atom = atom[0];
-          bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity;
-          if( !use_polarity ){
-            Assert(assert_active.find(fact) != assert_active.end());
-            if( assert_active[fact] ){
-              Assert(atom.getKind() == kind::SEP_LABEL);
-              TNode s_lbl = atom[1];
-              std::map<Node, std::map<int, Node> >& lms = d_label_map[s_atom];
-              if (lms.find(s_lbl) != lms.end())
-              {
-                Trace("sep-process-debug") << "Active lbl : " << s_lbl << std::endl;
-                active_lbl[s_lbl] = true;
-              }
-            }
-          }
-        }
-      }
+    Trace("sep-eqc") << std::endl;
+  }
 
-      //process spatial assertions
+  bool addedLemma = false;
+  bool needAddLemma = false;
+  // check negated star / positive wand
+  if (options::sepCheckNeg())
+  {
+    // get active labels
+    std::map<Node, bool> active_lbl;
+    if (options::sepMinimalRefine())
+    {
       for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
         Node fact = (*i);
-        bool polarity = fact.getKind() != kind::NOT;
+        bool polarity = fact.getKind() != NOT;
         TNode atom = polarity ? fact : fact[0];
-        TNode s_atom = atom[0];
-
-        bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity;
-        Trace("sep-process-debug") << "  check atom : " << s_atom << " use polarity " << use_polarity << std::endl;
+        TNode satom = atom[0];
+        bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity;
         if( !use_polarity ){
           Assert(assert_active.find(fact) != assert_active.end());
           if( assert_active[fact] ){
-            Assert(atom.getKind() == kind::SEP_LABEL);
-            TNode s_lbl = atom[1];
-            Trace("sep-process") << "--> Active negated atom : " << s_atom << ", lbl = " << s_lbl << std::endl;
-            //add refinement lemma
-            if (ContainsKey(d_label_map[s_atom], s_lbl))
-            {
-              needAddLemma = true;
-              TypeNode tn = getReferenceType( s_atom );
-              tn = NodeManager::currentNM()->mkSetType(tn);
-              //tn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn));
-              Node o_b_lbl_mval = d_label_model[s_lbl].getValue( tn );
-              Trace("sep-process") << "    Model for " << s_lbl << " : " << o_b_lbl_mval << std::endl;
-
-              //get model values
-              std::map< int, Node > mvals;
-              for (const std::pair<int, Node>& sub_element :
-                   d_label_map[s_atom][s_lbl])
-              {
-                int sub_index = sub_element.first;
-                Node sub_lbl = sub_element.second;
-                computeLabelModel( sub_lbl );
-                Node lbl_mval = d_label_model[sub_lbl].getValue( tn );
-                Trace("sep-process-debug") << "  child " << sub_index << " : " << sub_lbl << ", mval = " << lbl_mval << std::endl;
-                mvals[sub_index] = lbl_mval;
-              }
-
-              // Now, assert model-instantiated implication based on the negation
-              Assert(d_label_model.find(s_lbl) != d_label_model.end());
-              std::vector< Node > conc;
-              bool inst_success = true;
-              //new refinement
-              //instantiate the label
-              std::map< Node, Node > visited;
-              Node inst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, tn, active_lbl );
-              Trace("sep-inst-debug") << "    applied inst : " << inst << std::endl;
-              if( inst.isNull() ){
-                inst_success = false;
-              }else{
-                inst = Rewriter::rewrite( inst );
-                if( inst==( polarity ? d_true : d_false ) ){
-                  inst_success = false;
-                }
-                conc.push_back( polarity ? inst : inst.negate() );
-              }
-              if( inst_success ){
-                std::vector< Node > lemc;
-                Node pol_atom = atom;
-                if( polarity ){
-                  pol_atom = atom.negate();
-                }
-                lemc.push_back( pol_atom );
-
-                //lemc.push_back( s_lbl.eqNode( o_b_lbl_mval ).negate() );
-                //lemc.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, o_b_lbl_mval, s_lbl ).negate() );
-                lemc.insert( lemc.end(), conc.begin(), conc.end() );
-                Node lem = NodeManager::currentNM()->mkNode( kind::OR, lemc );
-                if( std::find( d_refinement_lem[s_atom][s_lbl].begin(), d_refinement_lem[s_atom][s_lbl].end(), lem )==d_refinement_lem[s_atom][s_lbl].end() ){
-                  d_refinement_lem[s_atom][s_lbl].push_back( lem );
-                  Trace("sep-process") << "-----> refinement lemma (#" << d_refinement_lem[s_atom][s_lbl].size() << ") : " << lem << std::endl;
-                  Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " << lem << std::endl;
-                  d_out->lemma( lem );
-                  addedLemma = true;
-                }else{
-                  //this typically should not happen, should never happen for complete base theories
-                  Trace("sep-process") << "*** repeated refinement lemma : " << lem << std::endl;
-                  Trace("sep-warn") << "TheorySep : WARNING : repeated refinement lemma : " << lem << "!!!" << std::endl;
-                }
-              }
-            }
-            else
+            Assert(atom.getKind() == SEP_LABEL);
+            TNode slbl = atom[1];
+            std::map<Node, std::map<int, Node> >& lms = d_label_map[satom];
+            if (lms.find(slbl) != lms.end())
             {
-              Trace("sep-process-debug") << "  no children." << std::endl;
-              Assert(s_atom.getKind() == kind::SEP_PTO
-                     || s_atom.getKind() == kind::SEP_EMP);
+              Trace("sep-process-debug")
+                  << "Active lbl : " << slbl << std::endl;
+              active_lbl[slbl] = true;
             }
-          }else{
-            Trace("sep-process-debug") << "--> inactive negated assertion " << s_atom << std::endl;
           }
         }
       }
-      Trace("sep-process") << "...finished check of negated assertions, addedLemma=" << addedLemma << ", needAddLemma=" << needAddLemma << std::endl;
     }
-    if( !addedLemma ){
-      //must witness finite data points-to
-      for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){
-        TypeNode data_type = d_loc_to_data_type[it->first];
-        //if the data type is finite
-        if( data_type.isInterpretedFinite() ){
-          computeLabelModel( it->second );
-          Trace("sep-process-debug") << "Check heap data for " << it->first << " -> " << data_type << std::endl;
-          for( unsigned j=0; j<d_label_model[it->second].d_heap_locs_model.size(); j++ ){
-            Assert(d_label_model[it->second].d_heap_locs_model[j].getKind()
-                   == kind::SINGLETON);
-            Node l = d_label_model[it->second].d_heap_locs_model[j][0];
-            Trace("sep-process-debug") << "  location : " << l << std::endl;
-            if( d_pto_model[l].isNull() ){
-              needAddLemma = true;
-              Node ll;
-              std::map< Node, Node >::iterator itm = d_tmodel.find( l );
-              if( itm!=d_tmodel.end() ) {
-                ll = itm->second;
-              }else{
-                //try to assign arbitrary skolem?
-              }
-              if( !ll.isNull() ){
-                Trace("sep-process") << "Must witness label : " << ll << ", data type is " << data_type << std::endl;
-                Node dsk = NodeManager::currentNM()->mkSkolem( "dsk", data_type, "pto-data for implicit location" );
-                // if location is in the heap, then something must point to it
-                Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, NodeManager::currentNM()->mkNode( kind::MEMBER, ll, it->second ), 
-                                                                            NodeManager::currentNM()->mkNode( kind::SEP_STAR,
-                                                                              NodeManager::currentNM()->mkNode( kind::SEP_PTO, ll, dsk ),
-                                                                              d_true ) );
-                Trace("sep-lemma") << "Sep::Lemma : witness finite data-pto : " << lem << std::endl;
-                d_out->lemma( lem );        
-                addedLemma = true;     
-              }else{
-                //This should only happen if we are in an unbounded fragment
-                Trace("sep-warn") << "TheorySep : WARNING : no term corresponding to location " << l << " in heap!!!" << std::endl;
-              }
-            }else{
-              Trace("sep-process-debug") << "  points-to data witness : " << d_pto_model[l] << std::endl;
-            }
-          }
-        }
+
+    // process spatial assertions
+    for (NodeList::const_iterator i = d_spatial_assertions.begin();
+         i != d_spatial_assertions.end();
+         ++i)
+    {
+      Node fact = (*i);
+      bool polarity = fact.getKind() != NOT;
+      TNode atom = polarity ? fact : fact[0];
+      TNode satom = atom[0];
+
+      bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity;
+      Trace("sep-process-debug")
+          << "  check atom : " << satom << " use polarity " << use_polarity
+          << std::endl;
+      if (use_polarity)
+      {
+        continue;
       }
-      if( !addedLemma ){
-        //set up model
-        Trace("sep-process-debug") << "...preparing sep model..." << std::endl;
-        d_heap_locs_nptos.clear();
-        //collect data points that are not pointed to
-        for( context::CDList<Assertion>::const_iterator it = facts_begin(); it != facts_end(); ++ it) {
-          Node lit = (*it).d_assertion;
-          if( lit.getKind()==kind::NOT && lit[0].getKind()==kind::SEP_PTO ){
-            Node s_atom = lit[0];
-            Node v1 = d_valuation.getModel()->getRepresentative( s_atom[0] );
-            Node v2 = d_valuation.getModel()->getRepresentative( s_atom[1] );
-            Trace("sep-process-debug") << v1 << " does not point-to " << v2 << std::endl;
-            d_heap_locs_nptos[v1].push_back( v2 );
-          }
-        }
-        
-        if( needAddLemma ){
-          d_out->setIncomplete();
+      Assert(assert_active.find(fact) != assert_active.end());
+      if (!assert_active[fact])
+      {
+        Trace("sep-process-debug")
+            << "--> inactive negated assertion " << satom << std::endl;
+        continue;
+      }
+      Assert(atom.getKind() == SEP_LABEL);
+      TNode slbl = atom[1];
+      Trace("sep-process") << "--> Active negated atom : " << satom
+                           << ", lbl = " << slbl << std::endl;
+      // add refinement lemma
+      if (!ContainsKey(d_label_map[satom], slbl))
+      {
+        Trace("sep-process-debug") << "  no children." << std::endl;
+        Assert(satom.getKind() == SEP_PTO || satom.getKind() == SEP_EMP);
+        continue;
+      }
+      needAddLemma = true;
+      TypeNode tn = getReferenceType(satom);
+      tn = nm->mkSetType(tn);
+      // tn = nm->mkSetType(nm->mkRefType(tn));
+      Node o_b_lbl_mval = d_label_model[slbl].getValue(tn);
+      Trace("sep-process") << "    Model for " << slbl << " : " << o_b_lbl_mval
+                           << std::endl;
+
+      // get model values
+      std::map<int, Node> mvals;
+      for (const std::pair<int, Node>& sub_element : d_label_map[satom][slbl])
+      {
+        int sub_index = sub_element.first;
+        Node sub_lbl = sub_element.second;
+        computeLabelModel(sub_lbl);
+        Node lbl_mval = d_label_model[sub_lbl].getValue(tn);
+        Trace("sep-process-debug")
+            << "  child " << sub_index << " : " << sub_lbl
+            << ", mval = " << lbl_mval << std::endl;
+        mvals[sub_index] = lbl_mval;
+      }
+
+      // Now, assert model-instantiated implication based on the negation
+      Assert(d_label_model.find(slbl) != d_label_model.end());
+      std::vector<Node> conc;
+      bool inst_success = true;
+      // new refinement
+      // instantiate the label
+      std::map<Node, Node> visited;
+      Node inst = instantiateLabel(satom,
+                                   slbl,
+                                   slbl,
+                                   o_b_lbl_mval,
+                                   visited,
+                                   d_pto_model,
+                                   tn,
+                                   active_lbl);
+      Trace("sep-inst-debug") << "    applied inst : " << inst << std::endl;
+      if (inst.isNull())
+      {
+        inst_success = false;
+      }
+      else
+      {
+        inst = Rewriter::rewrite(inst);
+        if (inst == (polarity ? d_true : d_false))
+        {
+          inst_success = false;
         }
+        conc.push_back(polarity ? inst : inst.negate());
+      }
+      if (!inst_success)
+      {
+        continue;
+      }
+      std::vector<Node> lemc;
+      Node pol_atom = atom;
+      if (polarity)
+      {
+        pol_atom = atom.negate();
+      }
+      lemc.push_back(pol_atom);
+      lemc.insert(lemc.end(), conc.begin(), conc.end());
+      Node lem = nm->mkNode(OR, lemc);
+      std::vector<Node>& rlems = d_refinement_lem[satom][slbl];
+      if (std::find(rlems.begin(), rlems.end(), lem) == rlems.end())
+      {
+        rlems.push_back(lem);
+        Trace("sep-process") << "-----> refinement lemma (#" << rlems.size()
+                             << ") : " << lem << std::endl;
+        Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : "
+                           << lem << std::endl;
+        d_out->lemma(lem);
+        addedLemma = true;
+      }
+      else
+      {
+        // this typically should not happen, should never happen for complete
+        // base theories
+        Trace("sep-process")
+            << "*** repeated refinement lemma : " << lem << std::endl;
+        Trace("sep-warn")
+            << "TheorySep : WARNING : repeated refinement lemma : " << lem
+            << "!!!" << std::endl;
       }
     }
+    Trace("sep-process")
+        << "...finished check of negated assertions, addedLemma=" << addedLemma
+        << ", needAddLemma=" << needAddLemma << std::endl;
+  }
+  if (addedLemma)
+  {
+    return;
+  }
+  // must witness finite data points-to
+  for (std::map<TypeNode, Node>::iterator it = d_base_label.begin();
+       it != d_base_label.end();
+       ++it)
+  {
+    TypeNode data_type = d_loc_to_data_type[it->first];
+    // if the data type is finite
+    if (!data_type.isInterpretedFinite())
+    {
+      continue;
+    }
+    computeLabelModel(it->second);
+    Trace("sep-process-debug") << "Check heap data for " << it->first << " -> "
+                               << data_type << std::endl;
+    std::vector<Node>& hlmodel = d_label_model[it->second].d_heap_locs_model;
+    for (size_t j = 0, hsize = hlmodel.size(); j < hsize; j++)
+    {
+      Assert(hlmodel[j].getKind() == SINGLETON);
+      Node l = hlmodel[j][0];
+      Trace("sep-process-debug") << "  location : " << l << std::endl;
+      if (!d_pto_model[l].isNull())
+      {
+        Trace("sep-process-debug")
+            << "  points-to data witness : " << d_pto_model[l] << std::endl;
+        continue;
+      }
+      needAddLemma = true;
+      Node ll;
+      std::map<Node, Node>::iterator itm = d_tmodel.find(l);
+      if (itm != d_tmodel.end())
+      {
+        ll = itm->second;
+      }
+      // otherwise, could try to assign arbitrary skolem?
+      if (!ll.isNull())
+      {
+        Trace("sep-process") << "Must witness label : " << ll
+                             << ", data type is " << data_type << std::endl;
+        Node dsk =
+            nm->mkSkolem("dsk", data_type, "pto-data for implicit location");
+        // if location is in the heap, then something must point to it
+        Node lem = nm->mkNode(
+            IMPLIES,
+            nm->mkNode(MEMBER, ll, it->second),
+            nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, ll, dsk), d_true));
+        Trace("sep-lemma") << "Sep::Lemma : witness finite data-pto : " << lem
+                           << std::endl;
+        d_out->lemma(lem);
+        addedLemma = true;
+      }
+      else
+      {
+        // This should only happen if we are in an unbounded fragment
+        Trace("sep-warn")
+            << "TheorySep : WARNING : no term corresponding to location " << l
+            << " in heap!!!" << std::endl;
+      }
+    }
+  }
+  if (addedLemma)
+  {
+    return;
+  }
+  // set up model
+  Trace("sep-process-debug") << "...preparing sep model..." << std::endl;
+  d_heap_locs_nptos.clear();
+  // collect data points that are not pointed to
+  for (context::CDList<Assertion>::const_iterator it = facts_begin();
+       it != facts_end();
+       ++it)
+  {
+    Node lit = (*it).d_assertion;
+    if (lit.getKind() == NOT && lit[0].getKind() == SEP_PTO)
+    {
+      Node satom = lit[0];
+      Node v1 = d_valuation.getModel()->getRepresentative(satom[0]);
+      Node v2 = d_valuation.getModel()->getRepresentative(satom[1]);
+      Trace("sep-process-debug")
+          << v1 << " does not point-to " << v2 << std::endl;
+      d_heap_locs_nptos[v1].push_back(v2);
+    }
   }
-  Trace("sep-check") << "Sep::check(): " << e << " done, conflict=" << d_conflict.get() << endl;
-}
 
+  if (needAddLemma)
+  {
+    d_out->setIncomplete();
+  }
+  Trace("sep-check") << "Sep::check(): " << level
+                     << " done, conflict=" << d_state.isInConflict()
+                     << std::endl;
+}
 
 bool TheorySep::needsCheckLastEffort() {
   return hasFacts();
@@ -849,7 +947,7 @@ void TheorySep::conflict(TNode a, TNode b) {
   std::vector<TNode> assumptions;
   explain(eq, assumptions);
   Node conflictNode = mkAnd(assumptions);
-  d_conflict = true;
+  d_state.notifyInConflict();
   d_out->conflict( conflictNode );
 }
 
@@ -1486,11 +1584,13 @@ void TheorySep::setInactiveAssertionRec( Node fact, std::map< Node, std::vector<
   assert_active[fact] = false;
   bool polarity = fact.getKind() != kind::NOT;
   TNode atom = polarity ? fact : fact[0];
-  TNode s_atom = atom[0];
-  TNode s_lbl = atom[1];
-  if( s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_STAR ){
-    for( unsigned j=0; j<s_atom.getNumChildren(); j++ ){
-      Node lblc = getLabel( s_atom, j, s_lbl );
+  TNode satom = atom[0];
+  TNode slbl = atom[1];
+  if (satom.getKind() == SEP_WAND || satom.getKind() == SEP_STAR)
+  {
+    for (size_t j = 0, nchild = satom.getNumChildren(); j < nchild; j++)
+    {
+      Node lblc = getLabel(satom, j, slbl);
       for( unsigned k=0; k<lbl_to_assertions[lblc].size(); k++ ){
         setInactiveAssertionRec( lbl_to_assertions[lblc][k], lbl_to_assertions, assert_active );
       }
@@ -1498,14 +1598,20 @@ void TheorySep::setInactiveAssertionRec( Node fact, std::map< Node, std::vector<
   }
 }
 
-void TheorySep::getLabelChildren( Node s_atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels ) {
-  for( unsigned i=0; i<s_atom.getNumChildren(); i++ ){
-    Node lblc = getLabel( s_atom, i, lbl );
+void TheorySep::getLabelChildren(Node satom,
+                                 Node lbl,
+                                 std::vector<Node>& children,
+                                 std::vector<Node>& labels)
+{
+  for (size_t i = 0, nchild = satom.getNumChildren(); i < nchild; i++)
+  {
+    Node lblc = getLabel(satom, i, lbl);
     Assert(!lblc.isNull());
     std::map< Node, Node > visited;
-    Node lc = applyLabel( s_atom[i], lblc, visited );
+    Node lc = applyLabel(satom[i], lblc, visited);
     Assert(!lc.isNull());
-    if( i==1 && s_atom.getKind()==kind::SEP_WAND ){
+    if (i == 1 && satom.getKind() == SEP_WAND)
+    {
       lc = lc.negate();
     }
     children.push_back( lc );
@@ -1621,8 +1727,9 @@ void TheorySep::validatePto( HeapAssertInfo * ei, Node ei_n ) {
       {
         TNode atom = fact[0];
         Assert(atom.getKind() == kind::SEP_LABEL);
-        TNode s_atom = atom[0];
-        if( s_atom.getKind()==kind::SEP_PTO ){
+        TNode satom = atom[0];
+        if (satom.getKind() == SEP_PTO)
+        {
           if( areEqual( atom[1], ei_n ) ){
             addPto( ei, ei_n, atom, false );
           }
@@ -1732,7 +1839,7 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c,
       if( conc==d_false ){
         Trace("sep-lemma") << "Sep::Conflict: " << ant_n << " by " << c << std::endl;
         d_out->conflict( ant_n );
-        d_conflict = true;
+        d_state.notifyInConflict();
       }else{
         Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant_n << " by " << c << std::endl;
         d_pending_exp.push_back( ant_n );
@@ -1746,7 +1853,8 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c,
 void TheorySep::doPendingFacts() {
   if( d_pending_lem.empty() ){
     for( unsigned i=0; i<d_pending.size(); i++ ){
-      if( d_conflict ){
+      if (d_state.isInConflict())
+      {
         break;
       }
       Node atom = d_pending[i].getKind()==kind::NOT ? d_pending[i][0] : d_pending[i];
@@ -1760,7 +1868,8 @@ void TheorySep::doPendingFacts() {
     }
   }else{
     for( unsigned i=0; i<d_pending_lem.size(); i++ ){
-      if( d_conflict ){
+      if (d_state.isInConflict())
+      {
         break;
       }
       int index = d_pending_lem[i];