Support for separation logic. Enable cbqi by default for pure BV.

34 files changed, 2526 insertions, 74 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index cfa4982ca..046b84f3a 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -446,7 +446,12 @@ libcvc4_la_SOURCES = \
 	theory/fp/theory_fp.cpp \
 	theory/fp/theory_fp_rewriter.h \
 	theory/fp/theory_fp_rewriter.cpp \
-	theory/fp/theory_fp_type_rules.h
+	theory/fp/theory_fp_type_rules.h \
+	theory/sep/theory_sep.h \
+	theory/sep/theory_sep.cpp \
+	theory/sep/theory_sep_rewriter.h \
+	theory/sep/theory_sep_rewriter.cpp \
+	theory/sep/theory_sep_type_rules.h
 
 nodist_libcvc4_la_SOURCES = \
 	theory/rewriter_tables.h \
diff --git a/src/Makefile.theories b/src/Makefile.theories
index 8b5cef4d5..003128a3c 100644
--- a/src/Makefile.theories
+++ b/src/Makefile.theories
@@ -1,3 +1,3 @@
 
 
-THEORIES = builtin booleans uf arith bv fp arrays datatypes sets strings quantifiers idl
+THEORIES = builtin booleans uf arith bv fp arrays datatypes sets sep strings quantifiers idl
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index c04de4421..9dcbc3b4b 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -40,6 +40,8 @@ libexpr_la_SOURCES = \
 	pickle_data.h \
 	pickler.cpp \
 	pickler.h \
+	sepconst.cpp \
+	sepconst.h \
 	symbol_table.cpp \
 	symbol_table.h \
 	type.cpp \
diff --git a/src/expr/sepconst.cpp b/src/expr/sepconst.cpp
new file mode 100644
index 000000000..7646b90d3
--- /dev/null
+++ b/src/expr/sepconst.cpp
@@ -0,0 +1,29 @@
+/*********************                                                        */
+/*! \file sepconst.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "expr/sepconst.h"
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const NilRef& asa) {
+  return out << "(nil " << asa.getType() << ")";
+}
+
+}/* CVC4 namespace */
diff --git a/src/expr/sepconst.h b/src/expr/sepconst.h
new file mode 100644
index 000000000..9f86c7efc
--- /dev/null
+++ b/src/expr/sepconst.h
@@ -0,0 +1,72 @@
+/*********************                                                        */
+/*! \file sepconst.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#pragma once
+
+namespace CVC4 {
+  // messy; Expr needs NilRef (because it's the payload of a
+  // CONSTANT-kinded expression), and NilRef needs Expr.
+  class CVC4_PUBLIC NilRef;
+  //class CVC4_PUBLIC EmpStar;
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+#include "expr/type.h"
+#include <iostream>
+
+namespace CVC4 {
+
+class CVC4_PUBLIC NilRef {
+  const Type d_type;
+  NilRef() { }
+public:
+  NilRef(Type refType):d_type(refType) { }
+
+  ~NilRef() throw() {
+  }
+  Type getType() const { return d_type; }
+  bool operator==(const NilRef& es) const throw() {
+    return d_type == es.d_type;
+  }
+  bool operator!=(const NilRef& es) const throw() {
+    return !(*this == es);
+  }
+  bool operator<(const NilRef& es) const throw() {
+    return d_type < es.d_type;
+  }
+  bool operator<=(const NilRef& es) const throw() {
+    return d_type <= es.d_type;
+  }
+  bool operator>(const NilRef& es) const throw() {
+    return !(*this <= es);
+  }
+  bool operator>=(const NilRef& es) const throw() {
+    return !(*this < es);
+  }
+};/* class NilRef */
+
+std::ostream& operator<<(std::ostream& out, const NilRef& es) CVC4_PUBLIC;
+
+struct CVC4_PUBLIC NilRefHashFunction {
+  inline size_t operator()(const NilRef& es) const {
+    return TypeHashFunction()(es.getType());
+  }
+};/* struct NilRefHashFunction */
+
+}/* CVC4 namespace */
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index e8a18481b..1eb84b45f 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -30,6 +30,7 @@ OPTIONS_SRC_FILES = \
 	proof_options \
 	prop_options \
 	quantifiers_options \
+	sep_options \
 	sets_options \
 	smt_options \
 	strings_options \
@@ -54,6 +55,7 @@ OPTIONS_TEMPS = \
 	proof_options.tmp \
 	prop_options.tmp \
 	quantifiers_options.tmp \
+	sep_options.tmp \
 	sets_options.tmp \
 	smt_options.tmp \
 	strings_options.tmp \
@@ -78,6 +80,7 @@ OPTIONS_OPTIONS_FILES = \
 	proof_options.options \
 	prop_options.options \
 	quantifiers_options.options \
+	sep_options.options \
 	sets_options.options \
 	smt_options.options \
 	strings_options.options \
@@ -102,6 +105,7 @@ OPTIONS_SEDS = \
 	proof_options.sed \
 	prop_options.sed \
 	quantifiers_options.sed \
+	sep_options.sed \
 	sets_options.sed \
 	smt_options.sed \
 	strings_options.sed \
@@ -126,6 +130,7 @@ OPTIONS_HEADS = \
 	proof_options.h \
 	prop_options.h \
 	quantifiers_options.h \
+	sep_options.h \
 	sets_options.h \
 	smt_options.h \
 	strings_options.h \
@@ -150,6 +155,7 @@ OPTIONS_CPPS = \
 	proof_options.cpp \
 	prop_options.cpp \
 	quantifiers_options.cpp \
+	sep_options.cpp \
 	sets_options.cpp \
 	smt_options.cpp \
 	strings_options.cpp \
@@ -295,14 +301,14 @@ options_holder_template.h options_template.cpp options_get_option_template.cpp o
 
 # Make sure the implicit rules never mistake X_options for the -o file for a
 # CPP file.
-arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sets_options smt_options strings_options theory_options uf_options:;
+arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sep_options sets_options smt_options strings_options theory_options uf_options:;
 
 
 # These are phony to force them to be made everytime.
-.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp
+.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sep_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp
 
 # Make is happier being listed explictly. Not sure why.
-arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp:
+arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sep_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp:
 	echo "$@" "$(@:.tmp=)"
 	$(AM_V_GEN)(cp "@srcdir@/$(@:.tmp=)" "$@" || true)
 #TIM:
diff --git a/src/options/sep_options b/src/options/sep_options
new file mode 100644
index 000000000..043355bda
--- /dev/null
+++ b/src/options/sep_options
@@ -0,0 +1,20 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module SEP "options/sep_options.h" Sep
+
+option sepCheckNeg --sep-check-neg bool :default true
+ check negated spatial assertions
+
+option sepExp --sep-exp bool :default false
+ experimental flag for sep
+option sepMinimalRefine --sep-min-refine bool :default false
+ only add refinement lemmas for minimal (innermost) assertions
+option sepPreciseBound --sep-prec-bound bool :default false
+ calculate precise bounds for labels
+option sepDisequalC --sep-deq-c bool :default true
+ assume cardinality elements are distinct
+
+endmodule
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 41428ed89..b3fe59b79 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1607,6 +1607,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         Debug("parser") << "Empty set encountered: " << f << " "
                           << f2 << " " << type <<  std::endl;
         expr = MK_CONST( ::CVC4::EmptySet(type) );
+      } else if(f.getKind() == CVC4::kind::NIL_REF) {
+        //hack: We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational.
+        //      However, the expression has 0 children. So we convert to (sep_nil tmp) here.
+        expr = MK_EXPR(CVC4::kind::SEP_NIL, PARSER_STATE->mkBoundVar("__tmp",type) );        
       } else {
         if(f.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
@@ -1911,6 +1915,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | EMPTYSET_TOK
     { expr = MK_CONST( ::CVC4::EmptySet(Type())); }
 
+  | NILREF_TOK
+    { expr = MK_CONST( ::CVC4::NilRef(Type())); }
     // NOTE: Theory constants go here
   ;
 
@@ -2646,6 +2652,7 @@ FMFCARDVAL_TOK : 'fmf.card.val';
 INST_CLOSURE_TOK : 'inst-closure';
 
 EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
+NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil';
 // Other set theory operators are not
 // tokenized and handled directly when
 // processing a term
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2da44152a..90fc11803 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -166,6 +166,18 @@ void Smt2::addFloatingPointOperators() {
   Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
 }
 
+void Smt2::addSepOperators() {
+  //addOperator(kind::SEP_NIL, "sep.nil");
+  addOperator(kind::SEP_STAR, "sep");
+  addOperator(kind::SEP_PTO, "pto");
+  addOperator(kind::SEP_WAND, "wand");
+  addOperator(kind::EMP_STAR, "emp");
+  //Parser::addOperator(kind::SEP_NIL);
+  Parser::addOperator(kind::SEP_STAR);
+  Parser::addOperator(kind::SEP_PTO);
+  Parser::addOperator(kind::SEP_WAND);
+  Parser::addOperator(kind::EMP_STAR);
+}
 
 void Smt2::addTheory(Theory theory) {
   switch(theory) {
@@ -254,7 +266,11 @@ void Smt2::addTheory(Theory theory) {
     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
     addFloatingPointOperators();
     break;
-
+    
+  case THEORY_SEP:
+    addSepOperators();
+    break;
+    
   default:
     std::stringstream ss;
     ss << "internal error: unsupported theory " << theory;
@@ -307,6 +323,8 @@ bool Smt2::isTheoryEnabled(Theory theory) const {
     return d_logic.isTheoryEnabled(theory::THEORY_UF);
   case THEORY_FP:
     return d_logic.isTheoryEnabled(theory::THEORY_FP);
+  case THEORY_SEP:
+    return d_logic.isTheoryEnabled(theory::THEORY_SEP);
   default:
     std::stringstream ss;
     ss << "internal error: unsupported theory " << theory;
@@ -415,6 +433,10 @@ void Smt2::setLogic(std::string name) {
     addTheory(THEORY_FP);
   }
 
+  if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
+    addTheory(THEORY_SEP);
+  }
+  
 }/* Smt2::setLogic() */
 
 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 1ae2c9dd7..b99e142ba 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -51,7 +51,8 @@ public:
     THEORY_SETS,
     THEORY_STRINGS,
     THEORY_UF,
-    THEORY_FP
+    THEORY_FP,
+    THEORY_SEP
   };
 
 private:
@@ -344,6 +345,7 @@ private:
 
   void addFloatingPointOperators();
 
+  void addSepOperators();
 };/* class Smt2 */
 
 }/* CVC4::parser namespace */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index f874074ac..7b6bc8708 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -318,7 +318,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     }
     return;
   }
-
+  
+  if( n.getKind() == kind::SEP_NIL ){
+    out << "sep.nil";
+    return;
+  }
+  
   bool stillNeedToPrintParams = true;
   bool forceBinary = false; // force N-ary to binary when outputing children
   // operator
@@ -581,6 +586,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::APPLY_SELECTOR_TOTAL:
   case kind::PARAMETRIC_DATATYPE:
     break;
+    
+  //separation
+  case kind::EMP_STAR:
+  case kind::SEP_PTO:
+  case kind::SEP_STAR:
+  case kind::SEP_WAND:out << smtKindString(k) << " "; break;
 
     // quantifiers
   case kind::FORALL:
@@ -853,6 +864,12 @@ static string smtKindString(Kind k) throw() {
   case kind::REGEXP_RANGE: return "re.range";
   case kind::REGEXP_LOOP: return "re.loop";
   
+  //sep theory
+  case kind::SEP_STAR: return "sep";
+  case kind::SEP_PTO: return "pto";
+  case kind::SEP_WAND: return "wand";
+  case kind::EMP_STAR: return "emp";
+    
   default:
     ; /* fall through */
   }
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 40b757598..8957ad7f7 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -458,7 +458,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         goto next_worklist;
       }
 
-      if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) {
+      if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean() && top.getKind()!=kind::SEP_STAR && top.getKind()!=kind::SEP_WAND) {
         // still need to rewrite e.g. function applications over boolean
         Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars);
         Node n;
@@ -682,20 +682,22 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
             goto next_worklist;
           }
         } else if(!t.isSort() && t.getNumChildren() > 0) {
-          for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
-            if((*i).isBoolean()) {
-              vector<TypeNode> argTypes(t.begin(), t.end());
-              replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType());
-              TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
-              Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
-                                    newType, "a variable introduced by Boolean-term conversion",
-                                    NodeManager::SKOLEM_EXACT_NAME);
-              Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-              top.setAttribute(BooleanTermAttr(), n);
-              d_varCache[top] = n;
-              result.top() << n;
-              worklist.pop();
-              goto next_worklist;
+          if( t.getKind()!=kind::SEP_STAR && t.getKind()!=kind::SEP_WAND ){
+            for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
+              if((*i).isBoolean()) {
+                vector<TypeNode> argTypes(t.begin(), t.end());
+                replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType());
+                TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
+                Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+                                      newType, "a variable introduced by Boolean-term conversion",
+                                      NodeManager::SKOLEM_EXACT_NAME);
+                Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+                top.setAttribute(BooleanTermAttr(), n);
+                d_varCache[top] = n;
+                result.top() << n;
+                worklist.pop();
+                goto next_worklist;
+              }
             }
           }
         }
@@ -714,6 +716,8 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
       case kind::RR_REWRITE:
       case kind::RR_DEDUCTION:
       case kind::RR_REDUCTION:
+      case kind::SEP_STAR:
+      case kind::SEP_WAND:
         // not yet supported
         result.top() << top;
         worklist.pop();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d5874c52f..69a150cc9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -94,6 +94,7 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/sort_inference.h"
 #include "theory/strings/theory_strings.h"
+#include "theory/sep/theory_sep.h"
 #include "theory/substitutions.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
@@ -1844,8 +1845,8 @@ void SmtEngine::setDefaults() {
     }
   }
   //counterexample-guided instantiation for non-sygus
-  // enable if any quantifiers with arithmetic or datatypes
-  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) ||
+  // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
+  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) || 
       options::cbqiAll() ){
     if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
@@ -3985,6 +3986,10 @@ void SmtEnginePrivate::processAssertions() {
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
     dumpAssertions("post-strings-pp", d_assertions);
   }
+  if( d_smt.d_logic.isTheoryEnabled(THEORY_SEP) ) {
+    //separation logic solver needs to register the entire input
+    ((theory::sep::TheorySep*)d_smt.d_theoryEngine->theoryOf(THEORY_SEP))->processAssertions( d_assertions.ref() );
+  }
   if( d_smt.d_logic.isQuantified() ){
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;
     //remove rewrite rules
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 00d337395..b7e973928 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -714,7 +714,8 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
     Assert (!value.isNull() || !fullModel);
 
     // may be a shared term that did not appear in the current assertions
-    if (!value.isNull()) {
+    // AJR: need to check whether already in map for cases where collectModelInfo is called multiple times in the same context
+    if (!value.isNull() && !d_modelMap->hasSubstitution(var)) {
       Debug("bitvector-model") << "   " << var << " => " << value << "\n";
       Assert (value.getKind() == kind::CONST_BITVECTOR);
       d_modelMap->addSubstitution(var, value);
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index d2637a555..523d868b5 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -190,7 +190,7 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit
 bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
-    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){
+    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() && !tn.isBitVector() ){
       if( options::cbqiSplx() ){
         return true;
       }else{
@@ -242,7 +242,7 @@ Node InstStrategyCbqi::getNextDecisionRequest(){
       Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
       bool value;
       if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
-        Trace("cbqi-debug2") << "CBQI: get next decision " << cel << std::endl;
+        Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl;
         return cel;
       }
     }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index f855154af..5d575969f 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -153,27 +153,23 @@ int ModelEngine::checkModel(){
   //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
 
   //for debugging
-  if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
-    for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
-         it != fm->d_rep_set.d_type_reps.end(); ++it ){
-      if( it->first.isSort() ){
-        Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
-        if( Trace.isOn("model-engine-debug") ){
-          Trace("model-engine-debug") << "        Reps : ";
-          for( size_t i=0; i<it->second.size(); i++ ){
-            Trace("model-engine-debug") << it->second[i] << "  ";
-          }
-          Trace("model-engine-debug") << std::endl;
-          Trace("model-engine-debug") << "   Term reps : ";
-          for( size_t i=0; i<it->second.size(); i++ ){
-            Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
-            Trace("model-engine-debug") << r << " ";
-          }
-          Trace("model-engine-debug") << std::endl;
-          Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
-          Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
-        }
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+       it != fm->d_rep_set.d_type_reps.end(); ++it ){
+    if( it->first.isSort() ){
+      Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+      Trace("model-engine-debug") << "        Reps : ";
+      for( size_t i=0; i<it->second.size(); i++ ){
+        Trace("model-engine-debug") << it->second[i] << "  ";
+      }
+      Trace("model-engine-debug") << std::endl;
+      Trace("model-engine-debug") << "   Term reps : ";
+      for( size_t i=0; i<it->second.size(); i++ ){
+        Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
+        Trace("model-engine-debug") << r << " ";
       }
+      Trace("model-engine-debug") << std::endl;
+      Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+      Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
     }
   }
 
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 437f1bddf..b9aab0236 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -382,7 +382,7 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int
 }
 
 void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
-  if( n.getKind()==AND || n.getKind()==OR ){
+  if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){
     newHasPol = hasPol;
     newPol = pol;
   }else if( n.getKind()==IMPLIES ){
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index c34d86497..9f222431e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1925,7 +1925,7 @@ bool TermDb::containsUninterpretedConstant( Node n ) {
     bool ret = false;
     if( n.getKind()==UNINTERPRETED_CONSTANT ){
       ret = true;
-    }else{
+    }else if( n.getKind()!=SEP_NIL ){  //sep.nil has dummy argument FIXME
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         if( containsUninterpretedConstant( n[i] ) ){
           ret = true;
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 802acc089..ee091919d 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -375,8 +375,13 @@ bool Trigger::isRelationalTriggerKind( Kind k ) {
 }
   
 bool Trigger::isCbqiKind( Kind k ) {
-  return quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ||
-         k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER;
+  if( quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){
+    return true;
+  }else{
+    //CBQI typically works for satisfaction-complete theories
+    TheoryId t = kindToTheoryId( k );
+    return t==THEORY_BV || t==THEORY_DATATYPES;
+  }
 }
 
 bool Trigger::isSimpleTrigger( Node n ){
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2bebabc5a..d81efe1da 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1041,16 +1041,20 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
 #ifdef CVC4_ASSERTIONS
     bool bad_inst = false;
     if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){
+      Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl;
       bad_inst = true;
     }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){
+      Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl;
       bad_inst = true;
     }else if( options::cbqi() ){
       Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
       if( !icf.isNull() ){
         if( icf==q ){
+          Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl;
+          bad_inst = true;
+        }else if( quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ) ){
+          Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl;
           bad_inst = true;
-        }else{
-          bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] );
         }
       }
     }
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds
new file mode 100644
index 000000000..52418aefb
--- /dev/null
+++ b/src/theory/sep/kinds
@@ -0,0 +1,37 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_SEP ::CVC4::theory::sep::TheorySep "theory/sep/theory_sep.h"
+typechecker "theory/sep/theory_sep_type_rules.h"
+
+properties polite stable-infinite parametric
+properties check propagate presolve getNextDecisionRequest
+
+# constants
+constant NIL_REF \
+    ::CVC4::NilRef \
+    ::CVC4::NilRefHashFunction \
+    "expr/sepconst.h" \
+    "the nil reference constant; payload is an instance of the CVC4::NilRef class"
+    
+rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h"
+
+operator SEP_NIL 1 "separation nil"
+operator EMP_STAR 1 "separation empty heap"
+operator SEP_PTO 2 "points to relation"
+operator SEP_STAR 2: "separation star"
+operator SEP_WAND 2 "separation magic wand"
+operator SEP_LABEL 2 "separation label"
+
+typerule NIL_REF ::CVC4::theory::sep::NilRefTypeRule
+typerule SEP_NIL ::CVC4::theory::sep::SepNilTypeRule
+typerule EMP_STAR ::CVC4::theory::sep::EmpStarTypeRule
+typerule SEP_PTO ::CVC4::theory::sep::SepPtoTypeRule
+typerule SEP_STAR ::CVC4::theory::sep::SepStarTypeRule
+typerule SEP_WAND ::CVC4::theory::sep::SepWandTypeRule
+typerule SEP_LABEL ::CVC4::theory::sep::SepLabelTypeRule
+
+endtheory
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
new file mode 100644
index 000000000..6fec57852
--- /dev/null
+++ b/src/theory/sep/theory_sep.cpp
@@ -0,0 +1,1502 @@
+/*********************                                                        */
+/*! \file theory_sep.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of the theory of sep.
+ **
+ ** Implementation of the theory of sep.
+ **/
+
+
+#include "theory/sep/theory_sep.h"
+#include "theory/valuation.h"
+#include "expr/kind.h"
+#include <map>
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
+#include "options/sep_options.h"
+#include "options/smt_options.h"
+#include "smt/logic_exception.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace sep {
+
+TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+  Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
+  d_notify(*this),
+  d_equalityEngine(d_notify, c, "theory::sep::TheorySep", true),
+  d_conflict(c, false),
+  d_reduce(u),
+  d_infer(c),
+  d_infer_exp(c),
+  d_spatial_assertions(c)
+{
+  d_true = NodeManager::currentNM()->mkConst<bool>(true);
+  d_false = NodeManager::currentNM()->mkConst<bool>(false);
+
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine.addFunctionKind(kind::SEP_PTO);
+  //d_equalityEngine.addFunctionKind(kind::SEP_STAR);
+}
+
+TheorySep::~TheorySep() {
+  for( std::map< Node, HeapAssertInfo * >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){
+    delete it->second;
+  }
+}
+
+void TheorySep::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
+Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) {
+  if( assumptions.empty() ){
+    return d_true;
+  }else if( assumptions.size()==1 ){
+    return assumptions[0];
+  }else{
+    return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
+  }
+}
+
+/////////////////////////////////////////////////////////////////////////////
+// PREPROCESSING
+/////////////////////////////////////////////////////////////////////////////
+
+
+
+Node TheorySep::ppRewrite(TNode term) {
+/*
+  Trace("sep-pp") << "ppRewrite : " << term << std::endl;
+  Node s_atom = term.getKind()==kind::NOT ? term[0] : term;
+  if( s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::EMP_STAR ){
+    //get the reference type (will compute d_type_references)
+    int card = 0;
+    TypeNode tn = getReferenceType( s_atom, card );
+    Trace("sep-pp") << "  reference type is " << tn << ", card is " << card << std::endl;
+  }
+*/
+  return term;
+}
+
+//must process assertions at preprocess so that quantified assertions are processed properly
+void TheorySep::processAssertions( std::vector< Node >& assertions ) {
+  std::map< Node, bool > visited;
+  for( unsigned i=0; i<assertions.size(); i++ ){
+    processAssertion( assertions[i], visited );
+  }
+}
+
+void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::EMP_STAR ){
+      //get the reference type (will compute d_type_references)
+      int card = 0;
+      TypeNode tn = getReferenceType( n, card );
+      Trace("sep-pp") << "  reference type is " << tn << ", card is " << card << std::endl;
+    }else{
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        processAssertion( n[i], visited );
+      }
+    }
+  }
+}
+
+Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+
+  return PP_ASSERT_STATUS_UNSOLVED;
+}
+
+
+/////////////////////////////////////////////////////////////////////////////
+// T-PROPAGATION / REGISTRATION
+/////////////////////////////////////////////////////////////////////////////
+
+
+bool TheorySep::propagate(TNode literal)
+{
+  Debug("sep") << "TheorySep::propagate(" << literal  << ")" << std::endl;
+  // If already in conflict, no more propagation
+  if (d_conflict) {
+    Debug("sep") << "TheorySep::propagate(" << literal << "): already in conflict" << std::endl;
+    return false;
+  }
+  bool ok = d_out->propagate(literal);
+  if (!ok) {
+    d_conflict = true;
+  }
+  return ok;
+}/* TheorySep::propagate(TNode) */
+
+
+void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
+  if( literal.getKind()==kind::SEP_LABEL ||
+      ( literal.getKind()==kind::NOT && literal[0].getKind()==kind::SEP_LABEL ) ){
+    //labelled assertions are never given to equality engine and should only come from the outside
+    assumptions.push_back( literal );
+  }else{
+    // Do the work
+    bool polarity = literal.getKind() != kind::NOT;
+    TNode atom = polarity ? literal : literal[0];
+    if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+      d_equalityEngine.explainEquality( atom[0], atom[1], polarity, assumptions, NULL );
+    } else {
+      d_equalityEngine.explainPredicate( atom, polarity, assumptions );
+    }
+  }
+}
+
+void TheorySep::preRegisterTerm(TNode node){
+
+}
+
+
+void TheorySep::propagate(Effort e){
+
+}
+
+
+Node TheorySep::explain(TNode literal)
+{
+  Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl;
+  std::vector<TNode> assumptions;
+  explain(literal, assumptions);
+  return mkAnd(assumptions);
+}
+
+
+/////////////////////////////////////////////////////////////////////////////
+// SHARING
+/////////////////////////////////////////////////////////////////////////////
+
+
+void TheorySep::addSharedTerm(TNode t) {
+  Debug("sep") << "TheorySep::addSharedTerm(" << 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) {
+    TNode a = d_sharedTerms[i];
+    TypeNode aType = a.getType();
+    for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
+      TNode b = d_sharedTerms[j];
+      if (b.getType() != aType) {
+        // We don't care about the terms of different types
+        continue;
+      }
+      switch (d_valuation.getEqualityStatus(a, b)) {
+      case EQUALITY_TRUE_AND_PROPAGATED:
+      case EQUALITY_FALSE_AND_PROPAGATED:
+        // If we know about it, we should have propagated it, so we can skip
+        break;
+      default:
+        // Let's split on it
+        addCarePair(a, b);
+        break;
+      }
+    }
+  }
+}
+
+
+/////////////////////////////////////////////////////////////////////////////
+// MODEL GENERATION
+/////////////////////////////////////////////////////////////////////////////
+
+
+void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel )
+{
+  // Send the equality engine information to the model
+  m->assertEqualityEngine( &d_equalityEngine );
+  
+  if( fullModel ){
+    for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){
+      computeLabelModel( it->second, d_tmodel );
+      //, (label = " << it->second << ")
+      Trace("sep-model") << "Model for heap, type = " << it->first << " : " << std::endl;
+      if( d_label_model[it->second].d_heap_locs_model.empty() ){
+        Trace("sep-model") << "  [empty]" << std::endl;
+      }else{
+        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-model") << "  " << l << " -> ";
+          if( d_pto_model[l].isNull() ){
+            Trace("sep-model") << "_";
+          }else{
+            Trace("sep-model") << d_pto_model[l];
+          }
+          Trace("sep-model") << std::endl;
+        }
+      }
+      Node nil = getNilRef( it->first );
+      Node vnil = d_valuation.getModel()->getRepresentative( nil );
+      Trace("sep-model") << "sep.nil = " << vnil << std::endl;
+      Trace("sep-model") << std::endl;
+    }
+  }
+}
+
+/////////////////////////////////////////////////////////////////////////////
+// NOTIFICATIONS
+/////////////////////////////////////////////////////////////////////////////
+
+
+void TheorySep::presolve() {
+  Trace("sep-pp") << "Presolving" << std::endl;
+  //TODO: cleanup if incremental?
+}
+
+
+/////////////////////////////////////////////////////////////////////////////
+// MAIN SOLVER
+/////////////////////////////////////////////////////////////////////////////
+
+
+void TheorySep::check(Effort e) {
+  if (done() && !fullEffort(e) && e != EFFORT_LAST_CALL) {
+    return;
+  }
+
+  getOutputChannel().spendResource(options::theoryCheckStep());
+
+  TimerStat::CodeTimer checkTimer(d_checkTime);
+  Trace("sep-check") << "Sep::check(): " << e << endl;
+
+  while( !done() && !d_conflict ){
+    // Get all the assertions
+    Assertion assertion = get();
+    TNode fact = assertion.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::EMP_STAR ){
+      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
+      }
+    }
+    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::EMP_STAR;
+    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
+        int card;
+        TypeNode refType = getReferenceType( s_atom, card );
+        Trace("sep-lemma-debug") << "...reference type is : " << refType << ", card is " << card << std::endl;
+        Node b_lbl = getBaseLabel( refType );
+        Node s_atom_new = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, s_atom, b_lbl );
+        Node lem;
+        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{
+      //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;
+          std::map< Node, Node >::iterator its = d_red_conc[s_lbl].find( s_atom );
+          if( its==d_red_conc[s_lbl].end() ){
+            //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;
+              int card;
+              TypeNode tn = getReferenceType( s_atom, card );
+              Assert( d_reference_bound.find( tn )!=d_reference_bound.end() );
+              c_lems.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, s_lbl, d_reference_bound[tn] ) );
+              if( options::sepPreciseBound() ){
+                //more precise bound
+                Trace("sep-bound") << "Propagate Bound(" << s_lbl << ") = ";
+                Assert( d_lbl_reference_bound.find( s_lbl )!=d_lbl_reference_bound.end() );
+                for( unsigned j=0; j<d_lbl_reference_bound[s_lbl].size(); j++ ){
+                  Trace("sep-bound") << d_lbl_reference_bound[s_lbl][j] << " ";
+                }
+                Trace("sep-bound") << std::endl << "  to children of " << s_atom << std::endl;
+                //int rb_start = 0;
+                for( unsigned j=0; j<s_atom.getNumChildren(); j++ ){
+                  int ccard = 0;
+                  getReferenceType( s_atom, ccard, j );
+                  Node c_lbl = getLabel( s_atom, j, s_lbl );
+                  Trace("sep-bound") << "  for " << c_lbl << ", card = " << ccard << " : ";
+                  std::vector< Node > bound_loc;
+                  bound_loc.insert( bound_loc.end(), d_references[s_atom][j].begin(), d_references[s_atom][j].end() );
+/*                //this is unsound
+                  for( int k=0; k<ccard; k++ ){
+                    Assert( rb_start<(int)d_lbl_reference_bound[s_lbl].size() );
+                    d_lbl_reference_bound[c_lbl].push_back( d_lbl_reference_bound[s_lbl][rb_start] );
+                    Trace("sep-bound") << d_lbl_reference_bound[s_lbl][rb_start] << " ";
+                    bound_loc.push_back( d_lbl_reference_bound[s_lbl][rb_start] );
+                    rb_start++;
+                  }
+*/
+                  //carry all locations for now
+                  bound_loc.insert( bound_loc.end(), d_lbl_reference_bound[s_lbl].begin(), d_lbl_reference_bound[s_lbl].end() );
+                  Trace("sep-bound") << std::endl;
+                  Node bound_v = mkUnion( tn, bound_loc );
+                  Trace("sep-bound") << "  ...bound value : " << bound_v << std::endl;
+                  children.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, c_lbl, bound_v ) );
+                }     
+                Trace("sep-bound") << "Done propagate Bound(" << s_lbl << ")" << std::endl;        
+              }
+              std::vector< Node > labels;
+              getLabelChildren( s_atom, s_lbl, children, labels );
+              Node empSet = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType()));
+              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 );
+              }
+              //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 );
+              }
+              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{
+              //labeled emp should be rewritten
+              Assert( false );
+            }
+            d_red_conc[s_lbl][s_atom] = conc;
+          }else{
+            conc = its->second;
+          }
+          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 lit = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
+              lit = getValuation().ensureLiteral( lit );
+              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_out->requirePhase( lit, true );
+              d_neg_guards.push_back( lit );
+              d_guard_to_assertion[lit] = s_atom;
+              //Node lem = NodeManager::currentNM()->mkNode( kind::IFF, 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 ant = atom;
+              if( polarity ){
+                ant = atom.negate();
+              }
+              Node lem = NodeManager::currentNM()->mkNode( kind::OR, ant, 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;
+          }
+        }
+      }
+      //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] );
+        if( polarity && s_lbl!=pto_lbl ){
+          //also propagate equality
+          Node eq = s_lbl.eqNode( pto_lbl );
+          Trace("sep-assert") << "Asserting implied equality " << eq << " to EE..." << std::endl;
+          d_equalityEngine.assertEquality(eq, true, fact);
+          Trace("sep-assert") << "Done asserting implied equality " << eq << " to EE." << std::endl;
+        }
+        //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 );
+      }
+    }
+  }
+
+  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;
+    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;
+          d_tmodel[v] = t;
+        }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-inst") << "Pto : " << s_atom[0] << " (" << vv << ") -> " << s_atom[1] << std::endl;
+            d_pto_model[vv] = s_atom[1];
+          }
+        }
+      }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;
+          }
+        }
+      }
+    }
+    //(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() != 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, d_tmodel );
+      }
+    }
+    //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") << "---" << 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-eqc") << " } " << std::endl;
+        ++eqcs2_i;
+      }
+      Trace("sep-eqc") << std::endl;
+    }
+
+    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];
+              if( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){
+                Trace("sep-process-debug") << "Active lbl : " << s_lbl << std::endl;
+                active_lbl[s_lbl] = true;
+              }
+            }
+          }
+        }
+      }
+
+      //process spatial assertions
+      bool addedLemma = false;
+      bool needAddLemma = false;
+      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;
+        Trace("sep-process-debug") << "  check atom : " << s_atom << " use polarity " << use_polarity << std::endl;
+        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( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){
+              needAddLemma = true;
+              int card;
+              TypeNode tn = getReferenceType( s_atom, card );
+              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( std::map< int, Node >::iterator itl = d_label_map[s_atom][s_lbl].begin(); itl != d_label_map[s_atom][s_lbl].end(); ++itl ){
+                Node sub_lbl = itl->second;
+                int sub_index = itl->first;
+                computeLabelModel( sub_lbl, d_tmodel );
+                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;
+              if( options::sepExp() ){
+                //old refinement lemmas
+                for( std::map< int, Node >::iterator itl = d_label_map[s_atom][s_lbl].begin(); itl != d_label_map[s_atom][s_lbl].end(); ++itl ){
+                  int sub_index = itl->first;
+                  std::map< Node, Node > visited;
+                  Node c = applyLabel( s_atom[itl->first], mvals[sub_index], visited );
+                  Trace("sep-process-debug") << "    applied inst : " << c << std::endl;
+                  if( s_atom.getKind()==kind::SEP_STAR || sub_index==0 ){
+                    conc.push_back( c.negate() );
+                  }else{
+                    conc.push_back( c );
+                  }
+                }
+              }else{
+                //new refinement
+                std::map< Node, Node > visited;
+                Node inst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, d_tmodel, 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{
+                  Trace("sep-process") << "*** repeated refinement lemma : " << lem << std::endl;
+                }
+              }
+            }else{
+              Trace("sep-process-debug") << "  no children." << std::endl;
+              Assert( s_atom.getKind()==kind::SEP_PTO );
+            }
+          }else{
+            Trace("sep-process-debug") << "--> inactive negated assertion " << s_atom << std::endl;
+          }
+        }
+      }
+      if( !addedLemma ){
+        if( needAddLemma ){
+          Trace("sep-process") << "WARNING : could not find refinement lemma!!!" << std::endl;
+          Assert( false );
+          d_out->setIncomplete();
+        }
+      }
+    }
+  }
+  Trace("sep-check") << "Sep::check(): " << e << " done, conflict=" << d_conflict.get() << endl;
+}
+
+
+Node TheorySep::getNextDecisionRequest() {
+  for( unsigned i=0; i<d_neg_guards.size(); i++ ){
+    Node g = d_neg_guards[i];
+    bool success = true;
+    if( getLogicInfo().isQuantified() ){
+      Assert( d_guard_to_assertion.find( g )!= d_guard_to_assertion.end() );
+      Node a = d_guard_to_assertion[g];
+      Node q = quantifiers::TermDb::getInstConstAttr( a );
+      if( !q.isNull() ){
+        //must wait to decide on counterexample literal from quantified formula
+        Node cel = getQuantifiersEngine()->getTermDatabase()->getCounterexampleLiteral( q );
+        bool value;
+        if( d_valuation.hasSatValue( cel, value ) ){
+          success = value;
+        }else{
+          Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : wait to decide on " << g << " until " << cel << " is set " << std::endl;
+          success = false;
+        }
+      }
+    }
+    if( success ){
+      bool value;
+      if( !d_valuation.hasSatValue( g, value ) ) {
+        Trace("sep-dec") << "TheorySep::getNextDecisionRequest : " << g << " (" << i << "/" << d_neg_guards.size() << ")" << std::endl;
+        return g;
+      }
+    }
+  }
+  Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : null" << std::endl;
+  return Node::null();
+}
+
+void TheorySep::conflict(TNode a, TNode b) {
+  Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl;
+  Node conflictNode;
+  if (a.getKind() == kind::CONST_BOOLEAN) {
+    conflictNode = explain(a.iffNode(b));
+  } else {
+    conflictNode = explain(a.eqNode(b));
+  }
+  d_conflict = true;
+  d_out->conflict( conflictNode );
+}
+
+
+TheorySep::HeapAssertInfo::HeapAssertInfo( context::Context* c ) : d_pto(c), d_has_neg_pto(c,false) {
+
+}
+
+TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) {
+  std::map< Node, HeapAssertInfo* >::iterator e_i = d_eqc_info.find( n );
+  if( e_i==d_eqc_info.end() ){
+    if( doMake ){
+      HeapAssertInfo* ei = new HeapAssertInfo( getSatContext() );
+      d_eqc_info[n] = ei;
+      return ei;
+    }else{
+      return NULL;
+    }
+  }else{
+    return (*e_i).second;
+  }
+}
+
+TypeNode TheorySep::getReferenceType( Node atom, int& card, int index ) {
+  Trace("sep-type") << "getReference type " << atom << " " << index << std::endl;
+  Assert( atom.getKind()==kind::SEP_PTO || atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND || atom.getKind()==kind::EMP_STAR || index!=-1 );
+  std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index );
+  if( it==d_reference_type[atom].end() ){
+    card = 0;
+    TypeNode tn;      
+    if( index==-1 && ( atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND ) ){
+      for( unsigned i=0; i<atom.getNumChildren(); i++ ){
+        int cardc = 0;
+        TypeNode ctn = getReferenceType( atom, cardc, i );
+        if( !ctn.isNull() ){
+          tn = ctn;
+        }
+        for( unsigned j=0; j<d_references[atom][i].size(); j++ ){
+          if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), d_references[atom][i][j] )==d_references[atom][index].end() ){
+            d_references[atom][index].push_back( d_references[atom][i][j] );
+          }
+        }
+        card = card + cardc;
+      }
+    }else{
+      Node n = index==-1 ? atom : atom[index];
+      //will compute d_references as well
+      std::map< Node, int > visited;
+      tn = getReferenceType2( atom, card, index, n, visited );
+    }
+    if( tn.isNull() && index==-1 ){
+      tn = NodeManager::currentNM()->booleanType();
+    }
+    d_reference_type[atom][index] = tn;
+    d_reference_type_card[atom][index] = card;
+    Trace("sep-type") << "...ref type return " << card << " for " << atom << " " << index << std::endl;
+    //add to d_type_references
+    if( index==-1 ){
+      //only contributes if top-level (index=-1)
+      for( unsigned i=0; i<d_references[atom][index].size(); i++ ){
+        Assert( !d_references[atom][index][i].isNull() );
+        if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), d_references[atom][index][i] )==d_type_references[tn].end() ){
+          d_type_references[tn].push_back( d_references[atom][index][i] );
+        }
+      }
+      // update maximum cardinality value
+      if( card>(int)d_card_max[tn] ){
+        d_card_max[tn] = card;
+      }
+    }
+    return tn;
+  }else{
+    Assert( d_reference_type_card[atom].find( index )!=d_reference_type_card[atom].end() );
+    card = d_reference_type_card[atom][index];
+    return it->second;
+  }
+}
+
+TypeNode TheorySep::getReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    Trace("sep-type-debug") << "visit : " << n << " : " << atom << " " << index << std::endl;
+    visited[n] = -1;
+    if( n.getKind()==kind::SEP_PTO ){
+      TypeNode tn1 = n[0].getType();
+      TypeNode tn2 = n[1].getType();
+      if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){
+        d_reference_bound_invalid[tn1] = true;
+      }else{
+        if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), n[0] )==d_references[atom][index].end() ){
+          d_references[atom][index].push_back( n[0] );
+        }
+      }
+      std::map< TypeNode, TypeNode >::iterator itt = d_loc_to_data_type.find( tn1 );
+      if( itt==d_loc_to_data_type.end() ){
+        Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl;
+        d_loc_to_data_type[tn1] = tn2;
+      }else{
+        if( itt->second!=tn2 ){
+          std::stringstream ss;
+          ss << "ERROR: location type " << tn1 << " is already associated with data type " << itt->second << ", offending atom is " << atom << " with data type " << tn2 << std::endl;
+          throw LogicException(ss.str());
+          Assert( false );
+        }
+      }
+      card = 1;
+      visited[n] = card;
+      return tn1;
+      //return n[1].getType();
+    }else if( n.getKind()==kind::EMP_STAR ){
+      card = 1;
+      visited[n] = card;
+      return n[0].getType();
+    }else if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND ){
+      Assert( n!=atom );
+      //get the references 
+      card = 0;
+      TypeNode tn = getReferenceType( n, card );
+      for( unsigned j=0; j<d_references[n][-1].size(); j++ ){
+        if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), d_references[n][-1][j] )==d_references[atom][index].end() ){
+          d_references[atom][index].push_back( d_references[n][-1][j] );
+        }
+      }
+      visited[n] = card;
+      return tn;
+    }else{
+      card = 0;
+      TypeNode otn;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        int cardc = 0;
+        TypeNode tn = getReferenceType2( atom, cardc, index, n[i], visited );
+        if( !tn.isNull() ){
+          otn = tn;
+        }
+        card = cardc>card ? cardc : card;
+      }
+      visited[n] = card;
+      return otn;
+    }
+  }else{
+    Trace("sep-type-debug") << "already visit : " << n << " : " << atom << " " << index << std::endl;
+    card = 0;
+    return TypeNode::null();
+  }
+}
+/*
+
+int TheorySep::getCardinality( Node n, std::vector< Node >& refs ) {
+  std::map< Node, int > visited;
+  return getCardinality2( n, refs, visited );
+}
+
+int TheorySep::getCardinality2( Node n, std::vector< Node >& refs, std::map< Node, int >& visited ) {
+  std::map< Node, int >::iterator it = visited.find( n );
+  if( it!=visited.end() ){
+    return it->second;
+  }else{
+    
+    
+  }
+}
+*/
+
+Node TheorySep::getBaseLabel( TypeNode tn ) {
+  std::map< TypeNode, Node >::iterator it = d_base_label.find( tn );
+  if( it==d_base_label.end() ){
+    Trace("sep") << "Make base label for " << tn << std::endl;
+    std::stringstream ss;
+    ss << "__Lb";
+    TypeNode ltn = NodeManager::currentNM()->mkSetType(tn);
+    //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn));
+    Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "" );
+    d_base_label[tn] = n_lbl;
+    //make reference bound
+    Trace("sep") << "Make reference bound label for " << tn << std::endl;
+    std::stringstream ss2;
+    ss2 << "__Lu";
+    d_reference_bound[tn] = NodeManager::currentNM()->mkSkolem( ss2.str(), ltn, "" );
+    d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), d_type_references[tn].end() );
+    //add a reference type for maximum occurrences of empty in a constraint
+    unsigned n_emp = d_card_max[tn]>d_card_max[TypeNode::null()] ? d_card_max[tn] : d_card_max[TypeNode::null()];
+    for( unsigned r=0; r<n_emp; r++ ){
+      Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
+      //d_type_references_all[tn].push_back( NodeManager::currentNM()->mkSkolem( "e", NodeManager::currentNM()->mkRefType(tn) ) );
+      if( options::sepDisequalC() ){
+        //ensure that it is distinct from all other references so far
+        for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){
+          Node eq = NodeManager::currentNM()->mkNode( e.getType().isBoolean() ? kind::IFF : kind::EQUAL, e, d_type_references_all[tn][j] );
+          d_out->lemma( eq.negate() );
+        }
+      }
+      d_type_references_all[tn].push_back( e );
+      d_lbl_reference_bound[d_base_label[tn]].push_back( e );
+    }
+    //construct bound
+    d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] );
+    Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl;
+
+    if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){
+      Node slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_reference_bound[tn], d_reference_bound_max[tn] );
+      Trace("sep-lemma") << "Sep::Lemma: reference bound for " << tn << " : " << slem << std::endl;
+      d_out->lemma( slem );
+    }else{
+      Trace("sep-bound") << "reference cannot be bound (possibly due to quantified pto)." << std::endl;
+    }
+    //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
+    //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl;
+    //d_out->lemma( slem );
+    return n_lbl;
+  }else{
+    return it->second;
+  }
+}
+
+Node TheorySep::getNilRef( TypeNode tn ) {
+  std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn );
+  if( it==d_nil_ref.end() ){
+    TypeEnumerator te(tn);
+    Node nil = NodeManager::currentNM()->mkNode( kind::SEP_NIL, *te );
+    d_nil_ref[tn] = nil;
+    return nil;
+  }else{
+    return it->second;
+  }
+}
+
+Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) {
+  Node u;
+  if( locs.empty() ){
+    TypeNode ltn = NodeManager::currentNM()->mkSetType(tn);
+    return NodeManager::currentNM()->mkConst(EmptySet(ltn.toType()));
+  }else{
+    for( unsigned i=0; i<locs.size(); i++ ){
+      Node s = locs[i];
+      Assert( !s.isNull() );
+      s = NodeManager::currentNM()->mkNode( kind::SINGLETON, s );
+      if( u.isNull() ){
+        u = s;
+      }else{
+        u = NodeManager::currentNM()->mkNode( kind::UNION, s, u );
+      }
+    }
+    return u;
+  }
+}
+
+Node TheorySep::getLabel( Node atom, int child, Node lbl ) {
+  std::map< int, Node >::iterator it = d_label_map[atom][lbl].find( child );
+  if( it==d_label_map[atom][lbl].end() ){
+    int card;
+    TypeNode refType = getReferenceType( atom, card );
+    std::stringstream ss;
+    ss << "__Lc" << child;
+    TypeNode ltn = NodeManager::currentNM()->mkSetType(refType);
+    //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(refType));
+    Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "" );
+    d_label_map[atom][lbl][child] = n_lbl;
+    d_label_map_parent[n_lbl] = lbl;
+    return n_lbl;
+  }else{
+    return (*it).second;
+  }
+}
+
+Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) {
+  Assert( n.getKind()!=kind::SEP_LABEL );
+  if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR ){
+    return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl );
+  }else if( !n.getType().isBoolean() || n.getNumChildren()==0 ){
+    return n;
+  }else{
+    std::map< Node, Node >::iterator it = visited.find( n );
+    if( it==visited.end() ){
+      std::vector< Node > children;
+      if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        children.push_back( n.getOperator() );
+      }
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node aln = applyLabel( n[i], lbl, visited );
+        children.push_back( aln );
+        childChanged = childChanged || aln!=n[i];
+      }
+      Node ret = n;
+      if( childChanged ){
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+      visited[n] = ret;
+      return ret;
+    }else{
+      return it->second;
+    }
+  }
+}
+
+Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, std::map< Node, Node >& tmodel,
+                                  TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind ) {
+  Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl;
+  if( options::sepMinimalRefine() && lbl!=o_lbl && active_lbl.find( lbl )!=active_lbl.end() ){
+    Trace("sep-inst") << "...do not instantiate " << o_lbl << " since it has an active sublabel " << lbl << std::endl;
+    return Node::null();
+  }else{
+    if( Trace.isOn("sep-inst") ){
+      if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND  || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR ){
+        for( unsigned j=0; j<ind; j++ ){ Trace("sep-inst") << "  "; }
+        Trace("sep-inst") << n << "[" << lbl << "] :: " << lbl_v << std::endl;
+      }
+    }
+    Assert( n.getKind()!=kind::SEP_LABEL );
+    if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND ){
+      if( lbl==o_lbl ){
+        std::vector< Node > children;
+        children.resize( n.getNumChildren() );
+        Assert( d_label_map[n].find( lbl )!=d_label_map[n].end() );
+        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;
+          Assert( sub_index>=0 && sub_index<(int)children.size() );
+          Trace("sep-inst-debug") << "Sublabel " << sub_index << " is " << sub_lbl << std::endl;
+          Node lbl_mval;
+          if( n.getKind()==kind::SEP_WAND && sub_index==1 ){
+            Assert( d_label_map[n][lbl].find( 0 )!=d_label_map[n][lbl].end() );
+            Node sub_lbl_0 = d_label_map[n][lbl][0];
+            computeLabelModel( sub_lbl_0, tmodel );
+            Assert( d_label_model.find( sub_lbl_0 )!=d_label_model.end() );
+            lbl_mval = NodeManager::currentNM()->mkNode( kind::UNION, lbl, d_label_model[sub_lbl_0].getValue( rtn ) );
+          }else{
+            computeLabelModel( sub_lbl, tmodel );
+            Assert( d_label_model.find( sub_lbl )!=d_label_model.end() );
+            lbl_mval = d_label_model[sub_lbl].getValue( rtn );
+          }
+          Trace("sep-inst-debug") << "Sublabel value is " << lbl_mval  << std::endl;
+          children[sub_index] = instantiateLabel( n[sub_index], o_lbl, sub_lbl, lbl_mval, visited, pto_model, tmodel, rtn, active_lbl, ind+1 );
+          if( children[sub_index].isNull() ){
+            return Node::null();
+          }
+        }
+        if( n.getKind()==kind::SEP_STAR ){
+          Assert( children.size()>1 );
+          return NodeManager::currentNM()->mkNode( kind::AND, children );      
+        }else{
+          return NodeManager::currentNM()->mkNode( kind::OR, children[0].negate(), children[1] );
+        }
+      }else{
+        //nested star/wand, label it and return
+        return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl_v );
+      }
+    }else if( n.getKind()==kind::SEP_PTO ){
+      //check if this pto reference is in the base label, if not, then it does not need to be added as an assumption
+      Assert( d_label_model.find( o_lbl )!=d_label_model.end() );
+      Node vr = d_valuation.getModel()->getRepresentative( n[0] );
+      Node svr = NodeManager::currentNM()->mkNode( kind::SINGLETON, vr );
+      bool inBaseHeap = std::find( d_label_model[o_lbl].d_heap_locs_model.begin(), d_label_model[o_lbl].d_heap_locs_model.end(), svr )!=d_label_model[o_lbl].d_heap_locs_model.end();
+      Trace("sep-inst-debug") << "Is in base (non-instantiating) heap : " << inBaseHeap << " for value ref " << vr << " in " << o_lbl << std::endl;
+      std::vector< Node > children;
+      if( inBaseHeap ){
+        Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] );
+        children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, n[0], n[1] ), s ) );
+      }else{
+        //look up value of data
+        std::map< Node, Node >::iterator it = pto_model.find( vr );
+        if( it!=pto_model.end() ){
+          if( n[1]!=it->second ){
+            children.push_back( NodeManager::currentNM()->mkNode( n[1].getType().isBoolean() ? kind::IFF : kind::EQUAL, n[1], it->second ) );
+          }
+        }else{
+          Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl;
+        }
+      } 
+      children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] ), lbl_v ) );
+      Node ret = children.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) );
+      Trace("sep-inst-debug") << "Return " << ret << std::endl;
+      return ret;
+    }else if( n.getKind()==kind::EMP_STAR ){
+      //return NodeManager::currentNM()->mkConst( lbl_v.getKind()==kind::EMPTYSET );
+      return lbl_v.eqNode( NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType().toType())) );
+    }else{
+      std::map< Node, Node >::iterator it = visited.find( n );
+      if( it==visited.end() ){
+        std::vector< Node > children;
+        if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+          children.push_back( n.getOperator() );
+        }
+        bool childChanged = false;
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          Node aln = instantiateLabel( n[i], o_lbl, lbl, lbl_v, visited, pto_model, tmodel, rtn, active_lbl, ind );
+          if( aln.isNull() ){
+            return Node::null();
+          }else{
+            children.push_back( aln );
+            childChanged = childChanged || aln!=n[i];
+          }
+        }
+        Node ret = n;
+        if( childChanged ){
+          ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+        }
+        //careful about caching
+        //visited[n] = ret;
+        return ret;
+      }else{
+        return it->second;
+      }
+    }
+  }
+}
+
+void TheorySep::setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active ) {
+  Trace("sep-process-debug") << "setInactiveAssertionRec::inactive : " << fact << std::endl;
+  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 );
+      for( unsigned k=0; k<lbl_to_assertions[lblc].size(); k++ ){
+        setInactiveAssertionRec( lbl_to_assertions[lblc][k], lbl_to_assertions, assert_active );
+      }
+    }
+  }
+}
+
+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 );
+    Assert( !lblc.isNull() );
+    std::map< Node, Node > visited;
+    Node lc = applyLabel( s_atom[i], lblc, visited );
+    Assert( !lc.isNull() );
+    if( i==1 && s_atom.getKind()==kind::SEP_WAND ){
+      lc = lc.negate();
+    }
+    children.push_back( lc );
+    labels.push_back( lblc );
+  }
+  Assert( children.size()>1 );
+}
+
+void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) {
+  if( !d_label_model[lbl].d_computed ){
+    d_label_model[lbl].d_computed = true;
+
+    //Node v_val = d_valuation.getModelValue( s_lbl );
+    //hack FIXME
+    Node v_val = d_valuation.getModel()->getRepresentative( lbl );
+    Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " << v_val << std::endl;
+    if( v_val.getKind()!=kind::EMPTYSET ){
+      while( v_val.getKind()==kind::UNION ){
+        Assert( v_val[1].getKind()==kind::SINGLETON );
+        d_label_model[lbl].d_heap_locs_model.push_back( v_val[1] );
+        v_val = v_val[0];
+      }
+      Assert( v_val.getKind()==kind::SINGLETON );
+      d_label_model[lbl].d_heap_locs_model.push_back( v_val );
+    }
+    //end hack
+    for( unsigned j=0; j<d_label_model[lbl].d_heap_locs_model.size(); j++ ){
+      Node u = d_label_model[lbl].d_heap_locs_model[j];
+      Assert( u.getKind()==kind::SINGLETON );
+      u = u[0];
+      Node tt;
+      std::map< Node, Node >::iterator itm = tmodel.find( u );
+      if( itm==tmodel.end() ) {
+        //Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << std::endl;
+        //Assert( false );
+        //tt = u;
+        //TypeNode tn = u.getType().getRefConstituentType();
+        TypeNode tn = u.getType();
+        Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << ", cref type " << tn << std::endl;
+        Assert( d_type_references_all.find( tn )!=d_type_references_all.end() && !d_type_references_all[tn].empty() );
+        tt = d_type_references_all[tn][0];
+      }else{
+        tt = itm->second;
+      }
+      Node stt = NodeManager::currentNM()->mkNode( kind::SINGLETON, tt );
+      Trace("sep-process-debug") << "...model : add " << tt << " for " << u << " in lbl " << lbl << std::endl;
+      d_label_model[lbl].d_heap_locs.push_back( stt );
+    }
+  }
+}
+
+Node TheorySep::getRepresentative( Node t ) {
+  if( d_equalityEngine.hasTerm( t ) ){
+    return d_equalityEngine.getRepresentative( t );
+  }else{
+    return t;
+  }
+}
+
+bool TheorySep::hasTerm( Node a ){
+  return d_equalityEngine.hasTerm( a );
+}
+
+bool TheorySep::areEqual( Node a, Node b ){
+  if( a==b ){
+    return true;
+  }else if( hasTerm( a ) && hasTerm( b ) ){
+    return d_equalityEngine.areEqual( a, b );
+  }else{
+    return false;
+  }
+}
+
+bool TheorySep::areDisequal( Node a, Node b ){
+  if( a==b ){
+    return false;
+  }else if( hasTerm( a ) && hasTerm( b ) ){
+    if( d_equalityEngine.areDisequal( a, b, false ) ){
+      return true;
+    }
+  }
+  return false;
+}
+
+void TheorySep::eqNotifyPreMerge(TNode t1, TNode t2) {
+
+}
+
+void TheorySep::eqNotifyPostMerge(TNode t1, TNode t2) {
+  HeapAssertInfo * e2 = getOrMakeEqcInfo( t2, false );
+  if( e2 && ( !e2->d_pto.get().isNull() || e2->d_has_neg_pto.get() ) ){
+    HeapAssertInfo * e1 = getOrMakeEqcInfo( t1, true );
+    if( !e2->d_pto.get().isNull() ){
+      if( !e1->d_pto.get().isNull() ){
+        Trace("sep-pto-debug") << "While merging " << t1 << " " << t2 << ", merge pto." << std::endl;
+        mergePto( e1->d_pto.get(), e2->d_pto.get() );
+      }else{
+        e1->d_pto.set( e2->d_pto.get() );
+      }
+    }
+    e1->d_has_neg_pto.set( e1->d_has_neg_pto.get() || e2->d_has_neg_pto.get() );
+    //validate
+    validatePto( e1, t1 );
+  }
+}
+
+void TheorySep::validatePto( HeapAssertInfo * ei, Node ei_n ) {
+  if( !ei->d_pto.get().isNull() && ei->d_has_neg_pto.get() ){
+    for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
+      Node fact = (*i);
+      bool polarity = fact.getKind() != kind::NOT;
+      if( !polarity ){
+        TNode atom = polarity ? fact : fact[0];
+        Assert( atom.getKind()==kind::SEP_LABEL );
+        TNode s_atom = atom[0];
+        if( s_atom.getKind()==kind::SEP_PTO ){
+          if( areEqual( atom[1], ei_n ) ){
+            addPto( ei, ei_n, atom, false );
+          }
+        }
+      }
+    }
+    //we have now processed all pending negated pto
+    ei->d_has_neg_pto.set( false );
+  }
+}
+
+void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ) {
+  Trace("sep-pto") << "Add pto " << p << ", pol = " << polarity << " to eqc " << ei_n << std::endl;
+  if( !ei->d_pto.get().isNull() ){
+    if( polarity ){
+      Trace("sep-pto-debug") << "...eqc " << ei_n << " already has pto " << ei->d_pto.get() << ", merge." << std::endl;
+      mergePto( ei->d_pto.get(), p );
+    }else{
+      Node pb = ei->d_pto.get();
+      Trace("sep-pto") << "Process positive/negated pto " << " " << pb << " " << p << std::endl;
+      Assert( pb.getKind()==kind::SEP_LABEL && pb[0].getKind()==kind::SEP_PTO );
+      Assert( p.getKind()==kind::SEP_LABEL && p[0].getKind()==kind::SEP_PTO );
+      Assert( areEqual( pb[1], p[1] ) );
+      std::vector< Node > exp;
+      if( pb[1]!=p[1] ){
+        exp.push_back( pb[1].eqNode( p[1] ) );
+      }
+      exp.push_back( pb );
+      exp.push_back( p.negate() );
+      std::vector< Node > conc;
+      if( pb[0][1]!=p[0][1] ){
+        conc.push_back( pb[0][1].eqNode( p[0][1] ).negate() );
+      }
+      if( pb[1]!=p[1] ){
+        conc.push_back( pb[1].eqNode( p[1] ).negate() );
+      }
+      Node n_conc = conc.empty() ? d_false : ( conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::OR, conc ) );
+      sendLemma( exp, n_conc, "PTO_NEG_PROP" );
+    }
+  }else{
+    if( polarity ){
+      ei->d_pto.set( p );
+      validatePto( ei, ei_n );
+    }else{
+      ei->d_has_neg_pto.set( true );
+    }
+  }
+}
+
+void TheorySep::mergePto( Node p1, Node p2 ) {
+  Trace("sep-lemma-debug") << "Merge pto " << p1 << " " << p2 << std::endl;
+  Assert( p1.getKind()==kind::SEP_LABEL && p1[0].getKind()==kind::SEP_PTO );
+  Assert( p2.getKind()==kind::SEP_LABEL && p2[0].getKind()==kind::SEP_PTO );
+  if( !areEqual( p1[0][1], p2[0][1] ) ){
+    std::vector< Node > exp;
+    if( p1[1]!=p2[1] ){
+      Assert( areEqual( p1[1], p2[1] ) );
+      exp.push_back( p1[1].eqNode( p2[1] ) );
+    }
+    exp.push_back( p1 );
+    exp.push_back( p2 );
+    sendLemma( exp, p1[0][1].eqNode( p2[0][1] ), "PTO_PROP" );
+  }
+}
+
+void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer ) {
+  Trace("sep-lemma-debug") << "Do rewrite on inference : " << conc << std::endl;
+  conc = Rewriter::rewrite( conc );
+  Trace("sep-lemma-debug") << "Got : " << conc << std::endl;
+  if( conc!=d_true ){
+    if( infer && conc!=d_false ){
+      Node ant_n;
+      if( ant.empty() ){
+        ant_n = d_true;
+      }else if( ant.size()==1 ){
+        ant_n = ant[0];
+      }else{
+        ant_n = NodeManager::currentNM()->mkNode( kind::AND, ant );
+      }
+      Trace("sep-lemma") << "Sep::Infer: " << conc << " from " << ant_n << " by " << c << std::endl;
+      d_pending_exp.push_back( ant_n );
+      d_pending.push_back( conc );
+      d_infer.push_back( ant_n );
+      d_infer_exp.push_back( conc );
+    }else{
+      std::vector< TNode > ant_e;
+      for( unsigned i=0; i<ant.size(); i++ ){
+        Trace("sep-lemma-debug") << "Explain : " << ant[i] << std::endl;
+        explain( ant[i], ant_e );
+      }
+      Node ant_n;
+      if( ant_e.empty() ){
+        ant_n = d_true;
+      }else if( ant_e.size()==1 ){
+        ant_n = ant_e[0];
+      }else{
+        ant_n = NodeManager::currentNM()->mkNode( kind::AND, ant_e );
+      }
+      if( conc==d_false ){
+        Trace("sep-lemma") << "Sep::Conflict: " << ant_n << " by " << c << std::endl;
+        d_out->conflict( ant_n );
+        d_conflict = true;
+      }else{
+        Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant_n << " by " << c << std::endl;
+        d_pending_exp.push_back( ant_n );
+        d_pending.push_back( conc );
+        d_pending_lem.push_back( d_pending.size()-1 );
+      }
+    }
+  }
+}
+
+void TheorySep::doPendingFacts() {
+  if( d_pending_lem.empty() ){
+    for( unsigned i=0; i<d_pending.size(); i++ ){
+      if( d_conflict ){
+        break;
+      }
+      Node atom = d_pending[i].getKind()==kind::NOT ? d_pending[i][0] : d_pending[i];
+      bool pol = d_pending[i].getKind()!=kind::NOT;
+      Trace("sep-pending") << "Sep : Assert to EE : " << atom << ", pol = " << pol << std::endl;
+      if( atom.getKind()==kind::EQUAL ){
+        d_equalityEngine.assertEquality(atom, pol, d_pending_exp[i]);
+      }else{
+        d_equalityEngine.assertPredicate(atom, pol, d_pending_exp[i]);
+      }
+    }
+  }else{
+    for( unsigned i=0; i<d_pending_lem.size(); i++ ){
+      if( d_conflict ){
+        break;
+      }
+      int index = d_pending_lem[i];
+      Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, d_pending_exp[index], d_pending[index] );
+      d_out->lemma( lem );
+      Trace("sep-pending") << "Sep : Lemma : " << lem << std::endl;
+    }
+  }
+  d_pending_exp.clear();
+  d_pending.clear();
+  d_pending_lem.clear();
+}
+
+void TheorySep::debugPrintHeap( HeapInfo& heap, const char * c ) {
+  Trace(c) << "[" << std::endl;
+  Trace(c) << "  ";
+  for( unsigned j=0; j<heap.d_heap_locs.size(); j++ ){
+    Trace(c) << heap.d_heap_locs[j] << " ";
+  }
+  Trace(c) << std::endl;
+  Trace(c) << "]" << std::endl;
+}
+
+Node TheorySep::HeapInfo::getValue( TypeNode tn ) {
+  Assert( d_heap_locs.size()==d_heap_locs_model.size() );
+  if( d_heap_locs.empty() ){
+    return NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
+  }else if( d_heap_locs.size()==1 ){
+    return d_heap_locs[0];
+  }else{
+    Node curr = NodeManager::currentNM()->mkNode( kind::UNION, d_heap_locs[0], d_heap_locs[1] );
+    for( unsigned j=2; j<d_heap_locs.size(); j++ ){
+      curr = NodeManager::currentNM()->mkNode( kind::UNION, curr, d_heap_locs[j] );
+    }
+    return curr;
+  }
+}
+
+}/* CVC4::theory::sep namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
new file mode 100644
index 000000000..506cb77cd
--- /dev/null
+++ b/src/theory/sep/theory_sep.h
@@ -0,0 +1,294 @@
+/*********************                                                        */
+/*! \file theory_sep.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Dejan Jovanovic, Clark Barrett
+ ** Minor contributors (to current version): Tim King, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Theory of sep
+ **
+ ** Theory of sep.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SEP__THEORY_SEP_H
+#define __CVC4__THEORY__SEP__THEORY_SEP_H
+
+#include "theory/theory.h"
+#include "util/statistics_registry.h"
+#include "theory/uf/equality_engine.h"
+#include "context/cdchunk_list.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/cdqueue.h"
+
+namespace CVC4 {
+namespace theory {
+
+class TheoryModel;
+
+namespace sep {
+
+class TheorySep : public Theory {
+  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+
+  /////////////////////////////////////////////////////////////////////////////
+  // MISC
+  /////////////////////////////////////////////////////////////////////////////
+
+  private:
+
+  /** True node for predicates = true */
+  Node d_true;
+
+  /** True node for predicates = false */
+  Node d_false;
+
+  Node mkAnd( std::vector< TNode >& assumptions );
+
+  void processAssertion( Node n, std::map< Node, bool >& visited );
+
+  public:
+
+  TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  ~TheorySep();
+
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
+  std::string identify() const { return std::string("TheorySep"); }
+
+  /////////////////////////////////////////////////////////////////////////////
+  // PREPROCESSING
+  /////////////////////////////////////////////////////////////////////////////
+
+  public:
+
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+  Node ppRewrite(TNode atom);
+  
+  void processAssertions( std::vector< Node >& assertions );
+  /////////////////////////////////////////////////////////////////////////////
+  // T-PROPAGATION / REGISTRATION
+  /////////////////////////////////////////////////////////////////////////////
+
+  private:
+
+  /** Should be called to propagate the literal.  */
+  bool propagate(TNode literal);
+
+  /** Explain why this literal is true by adding assumptions */
+  void explain(TNode literal, std::vector<TNode>& assumptions);
+
+  public:
+
+  void preRegisterTerm(TNode n);
+  void propagate(Effort e);
+  Node explain(TNode n);
+
+  public:
+
+  void addSharedTerm(TNode t);
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+  void computeCareGraph();
+
+  /////////////////////////////////////////////////////////////////////////////
+  // MODEL GENERATION
+  /////////////////////////////////////////////////////////////////////////////
+
+  public:
+
+  void collectModelInfo(TheoryModel* m, bool fullModel);
+
+  /////////////////////////////////////////////////////////////////////////////
+  // NOTIFICATIONS
+  /////////////////////////////////////////////////////////////////////////////
+
+  private:
+  public:
+
+  Node getNextDecisionRequest();
+
+  void presolve();
+  void shutdown() { }
+
+  /////////////////////////////////////////////////////////////////////////////
+  // MAIN SOLVER
+  /////////////////////////////////////////////////////////////////////////////
+  public:
+
+  void check(Effort e);
+
+  private:
+
+  // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
+  class NotifyClass : public eq::EqualityEngineNotify {
+    TheorySep& d_sep;
+  public:
+    NotifyClass(TheorySep& sep): d_sep(sep) {}
+
+    bool eqNotifyTriggerEquality(TNode equality, bool value) {
+      Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
+      // Just forward to sep
+      if (value) {
+        return d_sep.propagate(equality);
+      } else {
+        return d_sep.propagate(equality.notNode());
+      }
+    }
+
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+      Unreachable();
+    }
+
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+      Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
+      if (value) {
+        // Propagate equality between shared terms
+        return d_sep.propagate(t1.eqNode(t2));
+      } else {
+        return d_sep.propagate(t1.eqNode(t2).notNode());
+      }
+      return true;
+    }
+
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+      Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+      d_sep.conflict(t1, t2);
+    }
+
+    void eqNotifyNewClass(TNode t) { }
+    void eqNotifyPreMerge(TNode t1, TNode t2) { d_sep.eqNotifyPreMerge( t1, t2 ); }
+    void eqNotifyPostMerge(TNode t1, TNode t2) { d_sep.eqNotifyPostMerge( t1, t2 ); }
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+  };
+
+  /** The notify class for d_equalityEngine */
+  NotifyClass d_notify;
+
+  /** Equaltity engine */
+  eq::EqualityEngine d_equalityEngine;
+
+  /** Are we in conflict? */
+  context::CDO<bool> d_conflict;
+  std::vector< Node > d_pending_exp;
+  std::vector< Node > d_pending;
+  std::vector< int > d_pending_lem;
+
+  /** list of all refinement lemms */
+  std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem;
+
+  /** Conflict when merging constants */
+  void conflict(TNode a, TNode b);
+
+  //cache for positive polarity start reduction
+  NodeSet d_reduce;
+  std::map< Node, std::map< Node, Node > > d_red_conc;
+  std::map< Node, std::map< Node, Node > > d_neg_guard;
+  std::vector< Node > d_neg_guards;
+  std::map< Node, Node > d_guard_to_assertion;
+  //cache for references
+  std::map< Node, std::map< int, TypeNode > > d_reference_type;
+  std::map< Node, std::map< int, int > > d_reference_type_card;
+  std::map< Node, std::map< int, std::vector< Node > > > d_references;
+  /** inferences: maintained to ensure ref count for internally introduced nodes */
+  NodeList d_infer;
+  NodeList d_infer_exp;
+  NodeList d_spatial_assertions;
+
+  //currently fix one data type for each location type, throw error if using more than one
+  std::map< TypeNode, TypeNode > d_loc_to_data_type;
+  //information about types
+  std::map< TypeNode, Node > d_base_label;
+  std::map< TypeNode, Node > d_nil_ref;
+  //reference bound
+  std::map< TypeNode, Node > d_reference_bound;
+  std::map< TypeNode, Node > d_reference_bound_max;
+  std::map< TypeNode, bool > d_reference_bound_invalid;
+  std::map< TypeNode, std::vector< Node > > d_type_references;
+  std::map< TypeNode, std::vector< Node > > d_type_references_all;
+  std::map< TypeNode, unsigned > d_card_max;
+  //bounds for labels
+  std::map< Node, std::vector< Node > > d_lbl_reference_bound;
+  //for empty argument
+  std::map< TypeNode, Node > d_emp_arg;
+  //map from ( atom, label, child index ) -> label
+  std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map;
+  std::map< Node, Node > d_label_map_parent;
+
+  //term model
+  std::map< Node, Node > d_tmodel;
+  std::map< Node, Node > d_pto_model;
+
+  class HeapAssertInfo {
+  public:
+    HeapAssertInfo( context::Context* c );
+    ~HeapAssertInfo(){}
+    context::CDO< Node > d_pto;
+    context::CDO< bool > d_has_neg_pto;
+  };
+  std::map< Node, HeapAssertInfo * > d_eqc_info;
+  HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
+
+  //calculate the element type of the heap for spatial assertions
+  TypeNode getReferenceType( Node atom, int& card, int index = -1 );
+  TypeNode getReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited);
+  //get the base label for the spatial assertion
+  Node getBaseLabel( TypeNode tn );
+  Node getNilRef( TypeNode tn );
+  Node getLabel( Node atom, int child, Node lbl );
+  Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited );
+  void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels );
+
+  class HeapInfo {
+  public:
+    HeapInfo() : d_computed(false) {}
+    //information about the model
+    bool d_computed;
+    std::vector< Node > d_heap_locs;
+    std::vector< Node > d_heap_locs_model;
+    //get value
+    Node getValue( TypeNode tn );
+  };
+  //heap info ( label -> HeapInfo )
+  std::map< Node, HeapInfo > d_label_model;
+
+  void debugPrintHeap( HeapInfo& heap, const char * c );
+  void validatePto( HeapAssertInfo * ei, Node ei_n );
+  void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity );
+  void mergePto( Node p1, Node p2 );
+  void computeLabelModel( Node lbl, std::map< Node, Node >& tmodel );
+  Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, std::map< Node, Node >& tmodel, 
+                         TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 );
+  void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );
+
+  Node mkUnion( TypeNode tn, std::vector< Node >& locs );
+private:
+  Node getRepresentative( Node t );
+  bool hasTerm( Node a );
+  bool areEqual( Node a, Node b );
+  bool areDisequal( Node a, Node b );
+  /** called when two equivalence classes will merge */
+  void eqNotifyPreMerge(TNode t1, TNode t2);
+  void eqNotifyPostMerge(TNode t1, TNode t2);
+
+  void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false );
+  void doPendingFacts();
+public:
+  eq::EqualityEngine* getEqualityEngine() {
+    return &d_equalityEngine;
+  }
+
+};/* class TheorySep */
+
+}/* CVC4::theory::sep namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SEP__THEORY_SEP_H */
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
new file mode 100644
index 000000000..ce0b20cbd
--- /dev/null
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -0,0 +1,192 @@
+/*********************                                                        */
+/*! \file theory_sep_rewriter.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "expr/attribute.h"
+#include "theory/sep/theory_sep_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sep {
+
+void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ){
+  Assert( n.getKind()==kind::SEP_STAR );
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    if( n[i].getKind()==kind::EMP_STAR ){
+      s_children.push_back( n[i] );
+    }else if( n[i].getKind()==kind::SEP_STAR ){
+      getStarChildren( n[i], s_children, ns_children );
+    }else if( n[i].getKind()==kind::SEP_PTO ){
+      s_children.push_back( n[i] );
+    }else{
+      std::vector< Node > temp_s_children;
+      getAndChildren( n[i], temp_s_children, ns_children );
+      Node to_add;
+      if( temp_s_children.size()==0 ){
+        to_add = NodeManager::currentNM()->mkConst( true );
+      }else{
+        //remove empty star
+        std::vector< Node > temp_s_children2;
+        for( unsigned i=0; i<temp_s_children.size(); i++ ){
+          if( temp_s_children[i].getKind()!=kind::EMP_STAR ){
+            temp_s_children2.push_back( temp_s_children[i] );
+          }
+        }
+        if( temp_s_children2.size()==1 ){
+          to_add = temp_s_children2[0];
+        }else if( temp_s_children2.size()>1 ){
+          to_add = NodeManager::currentNM()->mkNode( kind::AND, temp_s_children2 );
+        }
+      }
+      if( !to_add.isNull() ){
+        //flatten star
+        if( to_add.getKind()==kind::SEP_STAR ){
+          getStarChildren( to_add, s_children, ns_children );
+        }else if( std::find( s_children.begin(), s_children.end(), to_add )==s_children.end() ){
+          s_children.push_back( to_add );
+        }
+      }
+    }
+  }
+}
+
+void TheorySepRewriter::getAndChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ) {
+  if( n.getKind()==kind::AND ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      getAndChildren( n[i], s_children, ns_children );
+    }
+  }else{
+    std::map< Node, bool > visited;
+    if( isSpatial( n, visited ) ){
+      if( std::find( s_children.begin(), s_children.end(), n )==s_children.end() ){
+        s_children.push_back( n );
+      }
+    }else{
+      if( std::find( ns_children.begin(), ns_children.end(), n )==ns_children.end() ){
+        if( n!=NodeManager::currentNM()->mkConst(true) ){
+          ns_children.push_back( n );
+        }
+      }
+    }
+  }
+}
+
+bool TheorySepRewriter::isSpatial( Node n, std::map< Node, bool >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR || n.getKind()==kind::SEP_LABEL ){
+      return true;
+    }else if( n.getType().isBoolean() ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( isSpatial( n[i], visited ) ){
+          return true;
+        }
+      }
+    }
+  }
+  return false;
+}
+
+RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
+  Trace("sep-postrewrite") << "Sep::postRewrite start " << node << std::endl;
+  Node retNode = node;
+  switch (node.getKind()) {
+    case kind::SEP_NIL: {
+      TypeEnumerator te(node[0].getType());
+      Node n = *te;
+      if( n!=node[0] ){
+        retNode = NodeManager::currentNM()->mkNode( kind::SEP_NIL, n );
+      }
+      break;
+    }
+    case kind::SEP_LABEL: {
+      if( node[0].getKind()==kind::SEP_PTO ){
+        Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, node[0][0] );
+        if( node[1]!=s ){
+          Node c1 = node[1].eqNode( s );
+          Node c2 = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, node[0][0], node[0][1] ), s );
+          retNode = NodeManager::currentNM()->mkNode( kind::AND, c1, c2 );
+        }
+      }
+      if( node[0].getKind()==kind::EMP_STAR ){
+        retNode = node[1].eqNode( NodeManager::currentNM()->mkConst(EmptySet(node[1].getType().toType())) );
+      }
+      break;
+    }
+    case kind::SEP_PTO: {
+      break;
+    }
+    case kind::SEP_STAR: {
+      //flatten
+      std::vector< Node > s_children;
+      std::vector< Node > ns_children;
+      getStarChildren( node, s_children, ns_children );
+      if( !s_children.empty() ){
+        Node schild;
+        if( s_children.size()==1 ) {
+          schild = s_children[0];
+        }else{
+          schild = NodeManager::currentNM()->mkNode( kind::SEP_STAR, s_children );
+        }
+        ns_children.push_back( schild );
+      }
+      Assert( !ns_children.empty() );
+      if( ns_children.size()==1 ){
+        retNode = ns_children[0];
+      }else{
+        retNode = NodeManager::currentNM()->mkNode( kind::AND, ns_children );
+      }
+      break;
+    }
+    case kind::EQUAL:
+    case kind::IFF: {
+      if(node[0] == node[1]) {
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+      }
+      else if (node[0].isConst() && node[1].isConst()) {
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
+      }
+      if (node[0] > node[1]) {
+        Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
+        return RewriteResponse(REWRITE_DONE, newNode);
+      }
+      break;
+    }
+    default:
+      break;
+  }
+  if( node!=retNode ){
+    Trace("sep-rewrite") << "Sep::rewrite : " << node << " -> " << retNode << std::endl;
+  }
+  return RewriteResponse(node==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
+}
+
+
+/*
+RewriteResponse TheorySepRewriter::preRewrite(TNode node) {
+  if( node.getKind()==kind::EMP_STAR ){
+    Trace("sep-prerewrite") << "Sep::preRewrite emp star " << std::endl;
+    return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkNode( kind::EMP_STAR, NodeManager::currentNM()->mkConst( true ) ) );
+  }else{
+    Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl;
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+}
+*/
+
+}/* CVC4::theory::sep namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h
new file mode 100644
index 000000000..02adbebe5
--- /dev/null
+++ b/src/theory/sep/theory_sep_rewriter.h
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file theory_sep_rewriter.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H
+#define __CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H
+
+#include "theory/rewriter.h"
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sep {
+
+
+class TheorySepRewriter {
+private:
+  static void getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children );
+  static void getAndChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children );
+  static bool isSpatial( Node n, std::map< Node, bool >& visited );
+public:
+
+  static RewriteResponse postRewrite(TNode node);
+  static inline RewriteResponse preRewrite(TNode node) {
+    Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl;
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  static inline void init() {}
+  static inline void shutdown() {}
+
+};/* class TheorySepRewriter */
+
+}/* CVC4::theory::sep namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H */
diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h
new file mode 100644
index 000000000..f47941b03
--- /dev/null
+++ b/src/theory/sep/theory_sep_type_rules.h
@@ -0,0 +1,136 @@
+/*********************                                                        */
+/*! \file theory_sep_type_rules.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Typing and cardinality rules for the theory of sep
+ **
+ ** Typing and cardinality rules for the theory of sep.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
+#define __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
+
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sep {
+
+class NilRefTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    return TypeNode::fromType( n.getConst<NilRef>().getType() );
+  }
+};
+
+class SepNilTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    return n[0].getType(check);    
+  }
+};
+
+class EmpStarTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    return nodeManager->booleanType();
+  }
+};
+
+struct SepPtoTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::SEP_PTO);
+    if( check ) {
+      TypeNode refType = n[0].getType(check);
+      //SEP-POLY
+      //if(!refType.isRef()) {
+      //  throw TypeCheckingExceptionPrivate(n, "pto applied to non-reference term");
+      //}
+      TypeNode ptType = n[1].getType(check);
+      //if(!ptType.isComparableTo(refType.getRefConstituentType())){
+      //  throw TypeCheckingExceptionPrivate(n, "pto maps reference to term of different type");
+      //}
+    }
+    return nodeManager->booleanType();
+  }
+};/* struct SepSelectTypeRule */
+
+struct SepStarTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TypeNode btype = nodeManager->booleanType();
+    Assert(n.getKind() == kind::SEP_STAR);
+    if( check ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        TypeNode ctype = n[i].getType( check );
+        if( ctype!=btype ){
+          throw TypeCheckingExceptionPrivate(n, "child of sep star is not Boolean");
+        }
+      }
+    }
+    return btype;
+  }
+};/* struct SepStarTypeRule */
+
+struct SepWandTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TypeNode btype = nodeManager->booleanType();
+    Assert(n.getKind() == kind::SEP_WAND);
+    if( check ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        TypeNode ctype = n[i].getType( check );
+        if( ctype!=btype ){
+          throw TypeCheckingExceptionPrivate(n, "child of sep magic wand is not Boolean");
+        }
+      }
+    }
+    return btype;
+  }
+};/* struct SepWandTypeRule */
+
+class EmpStarInternalTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    return nodeManager->booleanType();
+  }
+};/* struct EmpStarInternalTypeRule */
+
+struct SepLabelTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TypeNode btype = nodeManager->booleanType();
+    Assert(n.getKind() == kind::SEP_LABEL);
+    if( check ){
+      TypeNode ctype = n[0].getType( check );
+      if( ctype!=btype ){
+        throw TypeCheckingExceptionPrivate(n, "child of sep label is not Boolean");
+      }
+      TypeNode stype = n[1].getType( check );
+      if( !stype.isSet() ){
+        throw TypeCheckingExceptionPrivate(n, "label of sep label is not a set");
+      }
+    }
+    return btype;
+  }
+};/* struct SepLabelTypeRule */
+
+}/* CVC4::theory::sep namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 6b268805a..7b9786247 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -37,8 +37,13 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
 
   if( ( parent.getKind() == kind::FORALL ||
         parent.getKind() == kind::EXISTS ||
-        parent.getKind() == kind::REWRITE_RULE /*||
-        parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) &&
+        parent.getKind() == kind::REWRITE_RULE ||
+        parent.getKind() == kind::SEP_NIL ||
+        parent.getKind() == kind::SEP_STAR ||
+        parent.getKind() == kind::SEP_WAND ||
+        ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() )
+        // parent.getKind() == kind::CARDINALITY_CONSTRAINT
+      ) &&
       current != parent ) {
     Debug("register::internal") << "quantifier:true" << std::endl;
     return true;
@@ -177,8 +182,13 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 
   if( ( parent.getKind() == kind::FORALL ||
         parent.getKind() == kind::EXISTS ||
-        parent.getKind() == kind::REWRITE_RULE /*||
-        parent.getKind() == kind::CARDINALITY_CONSTRAINT*/  ) &&
+        parent.getKind() == kind::REWRITE_RULE ||
+        parent.getKind() == kind::SEP_NIL ||
+        parent.getKind() == kind::SEP_STAR ||
+        parent.getKind() == kind::SEP_WAND ||
+        ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() )
+        // parent.getKind() == kind::CARDINALITY_CONSTRAINT
+      ) &&
       current != parent ) {
     Debug("register::internal") << "quantifier:true" << std::endl;
     return true;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 382d4cf65..e8518b1f6 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -781,6 +781,14 @@ public:
   assertions_iterator facts_end() const {
     return d_facts.end();
   }
+  /**
+   * Whether facts have been asserted to this theory.
+   *
+   * @return true iff facts have been asserted to this theory.
+   */
+  bool hasFacts() { 
+    return !d_facts.empty(); 
+  }
 
   typedef context::CDList<TNode>::const_iterator shared_terms_iterator;
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 618fda4c0..78dca299f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -516,18 +516,29 @@ void TheoryEngine::check(Theory::Effort effort) {
 
     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
     if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
-      //d_theoryTable[THEORY_STRINGS]->check(Theory::EFFORT_LAST_CALL);
-      if(d_logicInfo.isQuantified()) {
-        // quantifiers engine must pass effort last call check
-        d_quantEngine->check(Theory::EFFORT_LAST_CALL);
-        // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
-      } else if(options::produceModels()) {
-        // must build model at this point
-        d_curr_model_builder->buildModel(d_curr_model, true);
+      //calls to theories requiring the model go here
+      //FIXME: this should not be theory-specific
+      if(d_logicInfo.isTheoryEnabled(THEORY_SEP)) {
+        Assert( d_theoryTable[THEORY_SEP]!=NULL );
+        if( d_theoryTable[THEORY_SEP]->hasFacts() ){
+          // must build model at this point
+          d_curr_model_builder->buildModel(getModel(), false);
+          d_theoryTable[THEORY_SEP]->check(Theory::EFFORT_LAST_CALL);
+        }
       }
-      Trace("theory::assertions-model") << endl;
-      if (Trace.isOn("theory::assertions-model")) {
-        printAssertions("theory::assertions-model");
+      if( ! d_inConflict && ! needCheck() ){
+        if(d_logicInfo.isQuantified()) {
+          // quantifiers engine must pass effort last call check
+          d_quantEngine->check(Theory::EFFORT_LAST_CALL);
+          // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
+        } else if(options::produceModels()) {
+          // must build model at this point
+          d_curr_model_builder->buildModel(getModel(), true);
+        }
+        Trace("theory::assertions-model") << endl;
+        if (Trace.isOn("theory::assertions-model")) {
+          printAssertions("theory::assertions-model");
+        }
       }
     }
 
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 6889d1002..a617f9455 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -561,7 +561,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   TheoryModel* tm = (TheoryModel*)m;
 
   // buildModel with fullModel = true should only be called once in any context
-  Assert(!tm->d_modelBuilt);
+  Assert(!tm->isBuilt());
   tm->d_modelBuilt = fullModel;
 
   // Reset model
@@ -1015,7 +1015,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
     retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
     if (childrenConst) {
       retNode = Rewriter::rewrite(retNode);
-      Assert(retNode.getKind()==kind::APPLY_UF || retNode.getKind()==kind::REGEXP_RANGE || retNode.isConst());
+      Assert(retNode.getKind()==kind::APPLY_UF || retNode.getKind()==kind::REGEXP_RANGE || retNode.getKind()==kind::SEP_NIL || retNode.isConst());
     }
   }
   d_normalizedCache[r] = retNode;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 6e4f77336..833b124eb 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -36,6 +36,7 @@ class TheoryModel : public Model
 protected:
   /** substitution map for this model */
   SubstitutionMap d_substitutions;
+  context::CDO<bool> d_modelBuilt;
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
   virtual ~TheoryModel() throw();
@@ -51,7 +52,6 @@ public:
   /** true/false nodes */
   Node d_true;
   Node d_false;
-  context::CDO<bool> d_modelBuilt;
   mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache;
 
 protected:
@@ -62,6 +62,8 @@ protected:
    */
   Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const;
 public:
+  /** is built */
+  bool isBuilt() { return d_modelBuilt.get(); }
   /**
    * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)
    * on this model.
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9c461f57b..ae935798e 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -551,9 +551,9 @@ void TheoryUF::eqNotifyNewClass(TNode t) {
 }
 
 void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) {
-  if (getLogicInfo().isQuantified()) {
+  //if (getLogicInfo().isQuantified()) {
     //getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 );
-  }
+  //}
 }
 
 void TheoryUF::eqNotifyPostMerge(TNode t1, TNode t2) {
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 165937c13..7e13668cd 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -87,6 +87,10 @@ Node Valuation::getModelValue(TNode var) {
   return d_engine->getModelValue(var);
 }
 
+TheoryModel* Valuation::getModel() {
+  return d_engine->getModel();
+}
+
 Node Valuation::ensureLiteral(TNode n) {
   return d_engine->ensureLiteral(n);
 }
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 4ecdecad0..54af14fdd 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -32,6 +32,7 @@ namespace theory {
 
 class EntailmentCheckParameters;
 class EntailmentCheckSideEffects;
+class TheoryModel;
 
 /**
  * The status of an equality in the current context.
@@ -106,6 +107,11 @@ public:
   Node getModelValue(TNode var);
 
   /**
+   * Returns pointer to model.
+   */
+  TheoryModel* getModel();
+  
+  /**
    * Ensure that the given node will have a designated SAT literal
    * that is definitionally equal to it.  The result of this function
    * is a Node that can be queried via getSatValue().