6 files changed, 29 insertions, 24 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 2dc3aebe5..6d8497a60 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -941,9 +941,10 @@ Expr ExprManager::mkBoundVar(Type type) {
   return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
 }
 
-Expr ExprManager::mkSepNil(Type type) {
+Expr ExprManager::mkUniqueVar(Type type, Kind k){
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode));
+  Node n = d_nodeManager->mkUniqueVar(*type.d_typeNode, k); 
+  return n.toExpr();
 }
 
 Expr ExprManager::mkAssociative(Kind kind,
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index f30b720de..95b9c60bf 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -547,9 +547,9 @@ public:
   Expr mkBoundVar(Type type);
   
   /**
-   * Create a (nameless) new nil reference for separation logic of type
+   * Create unique variable of type 
    */
-  Expr mkSepNil(Type type);
+  Expr mkUniqueVar( Type type, Kind k);
 
   /** Get a reference to the statistics registry for this ExprManager */
   Statistics getStatistics() const throw();
diff --git a/src/expr/node.h b/src/expr/node.h
index 998294da3..c9bfb75a4 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -308,7 +308,7 @@ public:
    * Destructor. If ref_count is true it will decrement the reference count
    * and, if zero, collect the NodeValue.
    */
-  ~NodeTemplate() throw(AssertionException);
+  ~NodeTemplate();
 
   /**
    * Return the null node.
@@ -1089,7 +1089,7 @@ NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
 }
 
 template <bool ref_count>
-NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
+NodeTemplate<ref_count>::~NodeTemplate() {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   if(ref_count) {
     // shouldn't ever fail
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index d2ac7e2a1..f7e76c06b 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -169,6 +169,8 @@ NodeManager::~NodeManager() {
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
     d_operators[i] = Node::null();
   }
+  
+  d_unique_vars.clear();
 
   //d_tupleAndRecordTypes.clear();
   d_tt_cache.d_children.clear();
@@ -681,18 +683,18 @@ Node NodeManager::mkInstConstant(const TypeNode& type) {
   return n;
 }
 
-Node NodeManager::mkSepNil(const TypeNode& type) {
-  Node n = NodeBuilder<0>(this, kind::SEP_NIL);
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(TypeCheckedAttr(), true);
-  return n;
-}
-
-Node* NodeManager::mkSepNilPtr(const TypeNode& type) {
-  Node* n = NodeBuilder<0>(this, kind::SEP_NIL).constructNodePtr();
-  setAttribute(*n, TypeAttr(), type);
-  setAttribute(*n, TypeCheckedAttr(), true);
-  return n;
+Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) {
+  std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
+  if( it==d_unique_vars[k].end() ){
+    Node n = NodeBuilder<0>(this, k);
+    n.setAttribute(TypeAttr(), type);
+    n.setAttribute(TypeCheckedAttr(), true);
+    d_unique_vars[k][type] = n;
+    Assert( n.getMetaKind() == kind::metakind::VARIABLE );
+    return n;
+  }else{
+    return it->second;
+  }
 }
 
 Node NodeManager::mkAbstractValue(const TypeNode& type) {
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index dcd7005f8..3c3636d5f 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -157,6 +157,9 @@ class NodeManager {
    * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
    */
   Node d_operators[kind::LAST_KIND];
+ 
+  /** unique vars per (Kind,Type) */
+  std::map< Kind, std::map< TypeNode, Node > > d_unique_vars;
 
   /**
    * A list of subscribers for NodeManager events.
@@ -486,13 +489,12 @@ public:
 
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
-  
-  /** Create nil reference for separation logic with the given type. */
-  Node mkSepNil(const TypeNode& type);
-  Node* mkSepNilPtr(const TypeNode& type);
 
   /** Make a new abstract value with the given type. */
   Node mkAbstractValue(const TypeNode& type);
+  
+  /** make unique (per Type,Kind) variable. */
+  Node mkUniqueVar(const TypeNode& type, Kind k);
 
   /**
    * Create a constant of type T.  It will have the appropriate
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 46fdaa143..0cada0df2 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -116,7 +116,7 @@ public:
    * Destructor. If ref_count is true it will decrement the reference count
    * and, if zero, collect the NodeValue.
    */
-  ~TypeNode() throw(AssertionException);
+  ~TypeNode();
 
   /**
    * Assignment operator for nodes, copies the relevant information from node
@@ -785,7 +785,7 @@ inline TypeNode::TypeNode(const TypeNode& typeNode) {
   d_nv->inc();
 }
 
-inline TypeNode::~TypeNode() throw(AssertionException) {
+inline TypeNode::~TypeNode() {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   d_nv->dec();
 }