Remove CDChunkList

CDChunkList was a version of CDList that could be allocated with the
ContextMemoryAllocator. None of the CDChunkList instances was using this
feature, so this commit changes them to CDLists. Additionally, the use
of CDChunkList was problematic: if a CDChunkList was created at a
non-zero context level and the context was popped below that level,
subsequent pushes would corrupt the context memory. This happened with
resetAssertions(), which pops down to level 0 while some CDChunkLists
were created at level 1. See also the added test case
"testPopBelowLevelCreated" for CDLists for illustration.

25 files changed, 101 insertions, 712 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index c78e75426..2691a34ae 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -36,7 +36,6 @@ libcvc4_la_SOURCES = \
 	git_versioninfo.cpp \
 	svn_versioninfo.cpp \
 	context/backtrackable.h \
-	context/cdchunk_list.h \
 	context/cddense_set.h \
 	context/cdhashmap.h \
 	context/cdhashmap_forward.h \
diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h
deleted file mode 100644
index d13c6ab90..000000000
--- a/src/context/cdchunk_list.h
+++ /dev/null
@@ -1,495 +0,0 @@
-/*********************                                                        */
-/*! \file cdchunk_list.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Context-dependent list class designed for use with a
- ** context memory allocator.
- **
- ** Context-dependent list class designed for use with a context
- ** memory allocator.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__CONTEXT__CDCHUNK_LIST_H
-#define __CVC4__CONTEXT__CDCHUNK_LIST_H
-
-#include <iterator>
-#include <memory>
-
-#include "base/cvc4_assert.h"
-#include "context/context.h"
-#include "context/context_mm.h"
-
-
-namespace CVC4 {
-namespace context {
-
-/**
- * Generic context-dependent dynamic array.  Like the usual CDList<>,
- * but allocates all memory from context memory.  Elements are kept in
- * cascading "list segments."  Access to elements by operator[] is not O(1) but
- * O(log n).  As with CDList<>, update is not permitted, only
- * appending to the end of the list.
- */
-template <class T>
-class CDChunkList : public ContextObj {
-public:
-
-  /** The value type with which this CDChunkList<> was instantiated. */
-  typedef T value_type;
-  /** The allocator type with which this CDChunkList<> was instantiated. */
-  typedef ContextMemoryAllocator<T> Allocator;
-
-protected:
-
-  static const size_t INITIAL_SEGMENT_SIZE = 10;
-  static const size_t INCREMENTAL_GROWTH_FACTOR = 2;
-
-  /**
-   * ListSegment is itself allocated in Context memory, but it is
-   * never updated; it serves as information about the d_list segment
-   * pointer it contains only.
-   */
-  class ListSegment {
-    ListSegment* d_nextSegment;
-    size_t d_segmentSize;
-    T* d_list;
-  public:
-    ListSegment() :
-      d_nextSegment(NULL),
-      d_segmentSize(0),
-      d_list(NULL) {
-    }
-    void initialize(T* list) {
-      Assert( d_nextSegment == NULL &&
-              d_segmentSize == 0 &&
-              d_list == NULL,
-              "Double-initialization of ListSegment not permitted" );
-      d_list = list;
-    }
-    void linkTo(ListSegment* nextSegment) {
-      Assert( d_nextSegment == NULL,
-              "Double-linking of ListSegment not permitted" );
-      d_nextSegment = nextSegment;
-    }
-    void cutLink() {
-      d_nextSegment = NULL;
-    }
-    ListSegment* getNextSegment() const { return d_nextSegment; }
-    size_t& size() { return d_segmentSize; }
-    size_t size() const { return d_segmentSize; }
-    const T* list() const { return d_list; }
-    T& operator[](size_t i) { return d_list[i]; }
-    const T& operator[](size_t i) const { return d_list[i]; }
-  };/* struct CDChunkList<T>::ListSegment */
-
-  /**
-   * The first segment of list memory.
-   */
-  ListSegment d_headSegment;
-
-  /**
-   * A pointer to the final segment of list memory.
-   */
-  ListSegment* d_tailSegment;
-
-  /**
-   * Whether to call the destructor when items are popped from the
-   * list.  True by default, but can be set to false by setting the
-   * second argument in the constructor to false.
-   */
-  bool d_callDestructor;
-
-  /**
-   * Number of objects in list across all segments.
-   */
-  size_t d_size;
-
-  /**
-   * Total allocated size across all segments.
-   */
-  size_t d_totalSizeAlloc;
-
-  /**
-   * Our allocator.
-   */
-  Allocator d_allocator;
-
-  /**
-   * Lightweight save object for CDChunkList<T, ContextMemoryAllocator<T> >.
-   */
-  struct CDChunkListSave : public ContextObj {
-    ListSegment* d_tail;
-    size_t d_tailSize, d_size, d_sizeAlloc;
-    CDChunkListSave(const CDChunkList<T>& list, ListSegment* tail,
-               size_t size, size_t sizeAlloc) :
-      ContextObj(list),
-      d_tail(tail),
-      d_tailSize(tail->size()),
-      d_size(size),
-      d_sizeAlloc(sizeAlloc) {
-    }
-    ~CDChunkListSave() {
-      this->destroy();
-    }
-    ContextObj* save(ContextMemoryManager* pCMM) {
-      // This type of object _is_ the save/restore object.  It isn't
-      // itself saved or restored.
-      Unreachable();
-    }
-    void restore(ContextObj* data) {
-      // This type of object _is_ the save/restore object.  It isn't
-      // itself saved or restored.
-      Unreachable();
-    }
-  };/* struct CDChunkList<T>::CDChunkListSave */
-
-  /**
-   * Private copy constructor undefined (no copy permitted).
-   */
-  CDChunkList(const CDChunkList<T>& l) CVC4_UNDEFINED;
-
-  /**
-   * Allocate the first list segment.
-   */
-  void allocateHeadSegment() {
-    Assert(d_headSegment.list() == NULL);
-    Assert(d_totalSizeAlloc == 0 && d_size == 0);
-
-    // Allocate an initial list if one does not yet exist
-    size_t newSize = INITIAL_SEGMENT_SIZE;
-    Debug("cdlist:cmm") << "initial grow of cdlist " << this
-                        << " level " << getContext()->getLevel()
-                        << " to " << newSize << std::endl;
-    if(newSize > d_allocator.max_size()) {
-      newSize = d_allocator.max_size();
-    }
-    T* newList = d_allocator.allocate(newSize);
-    if(newList == NULL) {
-      throw std::bad_alloc();
-    }
-    d_totalSizeAlloc = newSize;
-    d_headSegment.initialize(newList);
-  }
-
-  /**
-   * Allocate a new segment with more space.
-   * Throws bad_alloc if memory allocation fails.
-   */
-  void grow() {
-    Assert(d_totalSizeAlloc == d_size);
-
-    // Allocate a new segment
-    typedef typename Allocator::template rebind<ListSegment>::other
-      SegmentAllocator;
-    ContextMemoryManager* cmm = d_allocator.getCMM();
-    SegmentAllocator segAllocator = SegmentAllocator(cmm);
-    ListSegment* newSegment = segAllocator.allocate(1);
-    if(newSegment == NULL) {
-      throw std::bad_alloc();
-    }
-    segAllocator.construct(newSegment, ListSegment());
-    size_t newSize = INCREMENTAL_GROWTH_FACTOR * d_totalSizeAlloc;
-    if(newSize > d_allocator.max_size()) {
-      newSize = d_allocator.max_size();
-    }
-    T* newList = d_allocator.allocate(newSize);
-    Debug("cdlist:cmm") << "new segment of cdlistcontext " << this
-                        << " level " << getContext()->getLevel()
-                        << " to " << newSize
-                        << " (from " << d_tailSegment->list()
-                        << " to " << newList << ")" << std::endl;
-    if(newList == NULL) {
-      throw std::bad_alloc();
-    }
-    d_tailSegment->linkTo(newSegment);
-    d_tailSegment = newSegment;
-    d_tailSegment->initialize(newList);
-    d_totalSizeAlloc += newSize;
-  }
-
-  /**
-   * Implementation of mandatory ContextObj method save: simply copies the
-   * current size to a copy using the copy constructor (the pointer and the
-   * allocated size are *not* copied as they are not restored on a pop).
-   * The saved information is allocated using the ContextMemoryManager.
-   */
-  ContextObj* save(ContextMemoryManager* pCMM) {
-    ContextObj* data = new(pCMM) CDChunkListSave(*this, d_tailSegment,
-                                            d_size, d_totalSizeAlloc);
-    Debug("cdlist:cmm") << "save " << this
-                        << " at level " << this->getContext()->getLevel()
-                        << " size at " << this->d_size
-                        << " totalSizeAlloc at " << this->d_totalSizeAlloc
-                        << " data:" << data << std::endl;
-    return data;
-  }
-
-  /**
-   * Implementation of mandatory ContextObj method restore: simply restores the
-   * previous size.  Note that the list pointer and the allocated size are not
-   * changed.
-   */
-  void restore(ContextObj* data) {
-    CDChunkListSave* save = static_cast<CDChunkListSave*>(data);
-    Debug("cdlist:cmm") << "restore " << this
-                        << " level " << this->getContext()->getLevel()
-                        << " data == " << data
-                        << " call dtor == " << this->d_callDestructor
-                        << " d_tail == " << this->d_tailSegment << std::endl;
-    if(this->d_callDestructor) {
-      ListSegment* seg = &d_headSegment;
-      size_t i = save->d_size;
-      while(i >= seg->size()) {
-        i -= seg->size();
-        seg = seg->getNextSegment();
-      }
-      do {
-        while(i < seg->size()) {
-          this->d_allocator.destroy(&(*seg)[i++]);
-        }
-        i = 0;
-      } while((seg = seg->getNextSegment()) != NULL);
-    }
-
-    this->d_size = save->d_size;
-    this->d_tailSegment = save->d_tail;
-    this->d_tailSegment->size() = save->d_tailSize;
-    this->d_tailSegment->cutLink();
-    this->d_totalSizeAlloc = save->d_sizeAlloc;
-    Debug("cdlist:cmm") << "restore " << this
-                        << " level " << this->getContext()->getLevel()
-                        << " size back to " << this->d_size
-                        << " totalSizeAlloc at " << this->d_totalSizeAlloc
-                        << std::endl;
-  }
-
-public:
-
-  CDChunkList(Context* context, bool callDestructor, const Allocator& alloc) :
-    ContextObj(context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(alloc) {
-    allocateHeadSegment();
-  }
-
-  CDChunkList(Context* context, bool callDestructor = true) :
-    ContextObj(context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(Allocator(context->getCMM())) {
-    allocateHeadSegment();
-  }
-
-  CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor,
-         const Allocator& alloc) :
-    ContextObj(allocatedInCMM, context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(alloc) {
-    allocateHeadSegment();
-  }
-
-  CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
-    ContextObj(allocatedInCMM, context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(Allocator(context->getCMM())) {
-    allocateHeadSegment();
-  }
-
-  /**
-   * Destructor: delete the list
-   */
-  ~CDChunkList() {
-    this->destroy();
-
-    if(this->d_callDestructor) {
-      for(ListSegment* segment = &d_headSegment;
-          segment != NULL;
-          segment = segment->getNextSegment()) {
-        for(size_t i = 0; i < segment->size(); ++i) {
-          this->d_allocator.destroy(&(*segment)[i]);
-        }
-      }
-    }
-  }
-
-  /**
-   * Return the current size of (i.e. valid number of objects in) the
-   * list.
-   */
-  size_t size() const {
-    return d_size;
-  }
-
-  /**
-   * Return true iff there are no valid objects in the list.
-   */
-  bool empty() const {
-    return d_size == 0;
-  }
-
-  /**
-   * Add an item to the end of the list.
-   */
-  void push_back(const T& data) {
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " level " << getContext()->getLevel()
-                        << ": make-current, "
-                        << "d_list == " << d_tailSegment->list() << std::endl;
-    makeCurrent();
-
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " level " << getContext()->getLevel()
-                        << ": grow? " << d_size
-                        << " size_alloc " << d_totalSizeAlloc
-                        << std::endl;
-
-    if(d_size == d_totalSizeAlloc) {
-      Debug("cdlist:cmm") << "push_back " << this
-                          << " " << getContext()->getLevel()
-                          << ": grow!\n";
-      grow();
-    }
-    Assert(d_size < d_totalSizeAlloc);
-
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " " << getContext()->getLevel()
-                        << ": construct! at [" << d_size << "] == "
-                        << &(*d_tailSegment)[d_tailSegment->size()]
-                        << std::endl;
-    d_allocator.construct(&(*d_tailSegment)[d_tailSegment->size()], data);
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " " << getContext()->getLevel()
-                        << ": done..." << std::endl;
-    ++d_tailSegment->size();
-    ++d_size;
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " " << getContext()->getLevel()
-                        << ": size now " << d_size << std::endl;
-  }
-
-  /**
-   * Access to the ith item in the list in O(log n).
-   */
-  const T& operator[](size_t i) const {
-    Assert(i < d_size, "index out of bounds in CDChunkList::operator[]");
-    const ListSegment* seg = &d_headSegment;
-    while(i >= seg->size()) {
-      i -= seg->size();
-      seg = seg->getNextSegment();
-    }
-    return (*seg)[i];
-  }
-
-  /**
-   * Returns the most recent item added to the list.
-   */
-  const T& back() const {
-    Assert(d_size > 0, "CDChunkList::back() called on empty list");
-    return (*d_tailSegment)[d_tailSegment->size() - 1];
-  }
-
-  /**
-   * Iterator for CDChunkList class.  It has to be const because we don't
-   * allow items in the list to be changed.  It's a straightforward
-   * wrapper around a pointer.  Note that for efficiency, we implement
-   * only prefix increment and decrement.  Also note that it's OK to
-   * create an iterator from an empty, uninitialized list, as begin()
-   * and end() will have the same value (NULL).
-   */
-  class const_iterator {
-    const ListSegment* d_segment;
-    size_t d_index;
-
-    const_iterator(const ListSegment* segment, size_t i) :
-      d_segment(segment),
-      d_index(i) {
-    }
-
-    friend class CDChunkList<T>;
-
-  public:
-
-    typedef std::input_iterator_tag iterator_category;
-    typedef T value_type;
-    typedef std::ptrdiff_t difference_type;
-    typedef const T* pointer;
-    typedef const T& reference;
-
-    const_iterator() : d_segment(NULL), d_index(0) {}
-
-    inline bool operator==(const const_iterator& i) const {
-      return d_segment == i.d_segment && d_index == i.d_index;
-    }
-
-    inline bool operator!=(const const_iterator& i) const {
-      return !(*this == i);
-    }
-
-    inline const T& operator*() const {
-      return (*d_segment)[d_index];
-    }
-
-    /** Prefix increment */
-    const_iterator& operator++() {
-      if(++d_index >= d_segment->size()) {
-        d_segment = d_segment->getNextSegment();
-        d_index = 0;
-      }
-      return *this;
-    }
-
-    /** Postfix increment: returns new iterator with the old value. */
-    const_iterator operator++(int) {
-      const_iterator i = *this;
-      ++(*this);
-      return i;
-    }
-  };/* class CDChunkList<>::const_iterator */
-
-  /**
-   * Returns an iterator pointing to the first item in the list.
-   */
-  const_iterator begin() const {
-    // This looks curious, but we have to make sure that begin() == end()
-    // for an empty list, and begin() == (head,0) for a nonempty one.
-    // Since the segment spill-over is implemented in
-    // iterator::operator++(), let's reuse it. */
-    return ++const_iterator(&d_headSegment, -1);
-  }
-
-  /**
-   * Returns an iterator pointing one past the last item in the list.
-   */
-  const_iterator end() const {
-    return const_iterator(NULL, 0);
-  }
-};/* class CDChunkList<T, ContextMemoryAllocator<T> > */
-
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDCHUNK_LIST_H */
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 3dab675c3..aeb6567a3 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -419,7 +419,6 @@ public:
 template <class T, class CleanUp>
 class CDList<T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
   /* CDList is incompatible for use with a ContextMemoryAllocator.
-   * Consider using CDChunkList<T> instead.
    *
    * Explanation:
    * If ContextMemoryAllocator is used and d_list grows at a deeper context
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 9cfa7355d..099b45fec 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -22,9 +22,9 @@
 #include <iostream>
 #include <map>
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/datatype.h"
@@ -59,7 +59,6 @@ private:
   typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   IntMap d_testers;
   IntMap d_is_const;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 5166e118e..97c67e5e2 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -22,13 +22,13 @@
 #include <iostream>
 #include <map>
 
-#include "context/cdchunk_list.h"
+#include "context/cdlist.h"
+#include "expr/attribute.h"
 #include "expr/datatype.h"
 #include "theory/datatypes/datatypes_sygus.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 #include "util/hash.h"
-#include "expr/attribute.h"
 
 namespace CVC4 {
 namespace theory {
@@ -41,22 +41,22 @@ namespace datatypes {
 
 class TheoryDatatypes : public Theory {
 private:
-  typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
-  typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
+ typedef context::CDList<Node> NodeList;
+ typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
-  /** transitive closure to record equivalence/subterm relation.  */
-  //TransitiveClosureNode d_cycle_check;
-  /** has seen cycle */
-  context::CDO< bool > d_hasSeenCycle;
-  /** inferences */
-  NodeList d_infer;
-  NodeList d_infer_exp;
-  Node d_true;
-  Node d_zero;
-  /** mkAnd */
-  Node mkAnd( std::vector< TNode >& assumptions );
+ /** transitive closure to record equivalence/subterm relation.  */
+ // TransitiveClosureNode d_cycle_check;
+ /** has seen cycle */
+ context::CDO<bool> d_hasSeenCycle;
+ /** inferences */
+ NodeList d_infer;
+ NodeList d_infer_exp;
+ Node d_true;
+ Node d_zero;
+ /** mkAnd */
+ Node mkAnd(std::vector<TNode>& assumptions);
 private:
   //notification class for equality engine
   class NotifyClass : public eq::EqualityEngineNotify {
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index f0a3a85f5..c6dc2fd2f 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -23,7 +23,6 @@
 
 #include "context/context.h"
 #include "context/context_mm.h"
-#include "context/cdchunk_list.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h
index d69c94944..e0996d934 100644
--- a/src/theory/quantifiers/ce_guided_pbe.h
+++ b/src/theory/quantifiers/ce_guided_pbe.h
@@ -18,7 +18,6 @@
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H
 
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index ffcdb7075..7777ea2b9 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -18,7 +18,6 @@
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
 
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/ce_guided_single_inv_sol.h"
 #include "theory/quantifiers/inst_strategy_cbqi.h"
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h
index 61ade265f..c5f976f02 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h
@@ -18,7 +18,6 @@
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
 
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index e4246e2ab..1ebdaf649 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -18,7 +18,6 @@
 #define CONJECTURE_GENERATOR_H
 
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/type_enumerator.h"
 
@@ -229,7 +228,6 @@ class ConjectureGenerator : public QuantifiersModule
   friend class SubsEqcIndex;
   friend class TermGenerator;
   friend class TermGenEnv;
-  typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
 //this class maintains a congruence closure for *universal* facts
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 5b714c2d3..5a3f2e4d5 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.h
@@ -21,11 +21,10 @@
 #include <map>
 #include <vector>
 
-#include "context/context.h"
-#include "context/context_mm.h"
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
+#include "context/context.h"
+#include "context/context_mm.h"
 #include "theory/theory.h"
 
 
@@ -37,7 +36,7 @@ class EqualityInference
 {
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDList<Node> NodeList;
   typedef context::CDHashMap< Node, int, NodeHashFunction > NodeIntMap;
 private:
   context::Context * d_c;
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 794787bfc..40af2d030 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -18,9 +18,9 @@
 #define QUANT_CONFLICT_FIND
 
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
-#include "theory/quantifiers_engine.h"
+#include "context/cdlist.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -188,7 +188,6 @@ class QuantConflictFind : public QuantifiersModule
 {
   friend class MatchGen;
   friend class QuantInfo;
-  typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 private:
   context::CDO< bool > d_conflict;
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 34994f993..4e0b34ce8 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -18,7 +18,6 @@
 #ifndef __CVC4__REWRITE_ENGINE_H
 #define __CVC4__REWRITE_ENGINE_H
 
-#include "context/cdchunk_list.h"
 #include "context/context.h"
 #include "context/context_mm.h"
 #include "theory/quantifiers/trigger.h"
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
index 466e6d9a9..091490cec 100644
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ b/src/theory/quantifiers/symmetry_breaking.h
@@ -22,7 +22,6 @@
 #include <string>
 #include <vector>
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 #include "context/context.h"
 #include "context/context_mm.h"
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index ffede2a5b..d1d846628 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -22,8 +22,8 @@
 #include <memory>
 #include <unordered_map>
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
 #include "expr/attribute.h"
 #include "options/quantifiers_modes.h"
 #include "theory/quantifiers/inst_match.h"
@@ -101,8 +101,8 @@ class QuantifiersEngine {
   friend class quantifiers::QuantConflictFind;
   friend class inst::InstMatch;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDChunkList<bool> BoolList;
+  typedef context::CDList<Node> NodeList;
+  typedef context::CDList<bool> BoolList;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 private:
   /** reference to theory engine object */
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 1786584d4..591a495d0 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -19,13 +19,13 @@
 #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/cdlist.h"
 #include "context/cdqueue.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -35,7 +35,7 @@ class TheoryModel;
 namespace sep {
 
 class TheorySep : public Theory {
-  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDList<Node> NodeList;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index eb97405dc..d6e52a308 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -19,8 +19,8 @@
 
 #include <unordered_set>
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
 #include "theory/sets/rels_utils.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -46,8 +46,7 @@ public:
 };/* class TupleTrie */
 
 class TheorySetsRels {
-
-  typedef context::CDChunkList< Node >                            NodeList;
+  typedef context::CDList<Node> NodeList;
   typedef context::CDHashSet< Node, NodeHashFunction >            NodeSet;
   typedef context::CDHashMap< Node, Node, NodeHashFunction >      NodeMap;
 
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 0bdaf7ab5..39ab70e2f 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -19,14 +19,13 @@
 #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
 #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
 
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/strings/theory_strings_preprocess.h"
-#include "theory/strings/regexp_operation.h"
-
-#include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
 #include "expr/attribute.h"
+#include "theory/strings/regexp_operation.h"
+#include "theory/strings/theory_strings_preprocess.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
 
 #include <climits>
 #include <deque>
@@ -49,7 +48,7 @@ struct StringsProxyVarAttributeId {};
 typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
 
 class TheoryStrings : public Theory {
-  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDList<Node> NodeList;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 60bfd6fab..41987265e 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -23,7 +23,6 @@
 #include "util/hash.h"
 #include "theory/theory.h"
 #include "theory/rewriter.h"
-#include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 
 namespace CVC4 {
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index a7239dba5..0166bd947 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -17,7 +17,6 @@
 #ifndef __CVC4__THEORY_UF_STRONG_SOLVER_H
 #define __CVC4__THEORY_UF_STRONG_SOLVER_H
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 #include "context/context.h"
 #include "context/context_mm.h"
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 55a6c2b09..1be242e3d 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -3,6 +3,7 @@ TEST_EXTENSIONS = .class
 CPLUSPLUS_TESTS = \
 	boilerplate \
 	ouroborous \
+	reset_assertions \
 	two_smt_engines \
 	smt2_compliance \
 	statistics
diff --git a/test/system/reset_assertions.cpp b/test/system/reset_assertions.cpp
new file mode 100644
index 000000000..4fed06698
--- /dev/null
+++ b/test/system/reset_assertions.cpp
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file reset_assertions.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A simple test for SmtEngine::resetAssertions()
+ **
+ ** This program indirectly also tests some corner cases w.r.t.
+ ** context-dependent datastructures: resetAssertions() pops the contexts to
+ ** zero but some context-dependent datastructures are created at leevel 1,
+ ** which the datastructure needs to handle properly problematic.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+
+int main()
+{
+  ExprManager em;
+  SmtEngine smt(&em);
+
+  smt.setOption("incremental", SExpr(true));
+
+  Type real = em.realType();
+  Expr x = em.mkVar("x", real);
+  Expr four = em.mkConst(Rational(4));
+  Expr xEqFour = em.mkExpr(Kind::EQUAL, x, four);
+  smt.assertFormula(xEqFour);
+  std::cout << smt.checkSat() << std::endl;
+
+  smt.resetAssertions();
+
+  Type elementType = em.integerType();
+  Type indexType = em.integerType();
+  Type arrayType = em.mkArrayType(indexType, elementType);
+  Expr array = em.mkVar("array", arrayType);
+  Expr arrayAtFour = em.mkExpr(Kind::SELECT, array, four);
+  Expr ten = em.mkConst(Rational(10));
+  Expr arrayAtFour_eq_ten = em.mkExpr(Kind::EQUAL, arrayAtFour, ten);
+  smt.assertFormula(arrayAtFour_eq_ten);
+  std::cout << smt.checkSat() << std::endl;
+}
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 9640a059a..a14267fff 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -33,7 +33,6 @@ UNIT_TESTS += \
 	context/context_mm_black \
 	context/cdo_black \
 	context/cdlist_black \
-	context/cdlist_context_memory_black \
 	context/cdmap_black \
 	context/cdmap_white \
 	context/cdvector_black \
diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index 8525ef6f3..5015ae002 100644
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -150,4 +150,12 @@ class CDListBlack : public CxxTest::TestSuite {
 
 #endif /* CVC4_MEMORY_LIMITING_DISABLED */
   }
+
+  void testPopBelowLevelCreated()
+  {
+    d_context->push();
+    CDList<int> list(d_context);
+    d_context->popto(0);
+    list.push_back(42);
+  }
 };
diff --git a/test/unit/context/cdlist_context_memory_black.h b/test/unit/context/cdlist_context_memory_black.h
deleted file mode 100644
index 654251a0c..000000000
--- a/test/unit/context/cdlist_context_memory_black.h
+++ /dev/null
@@ -1,160 +0,0 @@
-/*********************                                                        */
-/*! \file cdlist_context_memory_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::context::CDList<>.
- **
- ** Black box testing of CVC4::context::CDList<>.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <vector>
-
-#include <limits.h>
-
-#include "memory.h"
-
-#include "context/cdchunk_list.h"
-#include "context/context.h"
-
-using namespace std;
-using namespace CVC4::context;
-
-struct DtorSensitiveObject {
-  bool& d_dtorCalled;
-  DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {}
-  ~DtorSensitiveObject() { d_dtorCalled = true; }
-};
-
-class CDListContextMemoryBlack : public CxxTest::TestSuite {
- private:
-  Context* d_context;
-
- public:
-  void setUp() { d_context = new Context(); }
-
-  void tearDown() { delete d_context; }
-
-  // test at different sizes.  this triggers grow() behavior differently.
-  // grow() was completely broken in revision 256
-  void testCDChunkList10() { listTest(10); }
-  void testCDChunkList15() { listTest(15); }
-  void testCDChunkList20() { listTest(20); }
-  void testCDChunkList35() { listTest(35); }
-  void testCDChunkList50() { listTest(50); }
-  void testCDChunkList99() { listTest(99); }
-
-  void listTest(int N) {
-    listTest(N, true);
-    listTest(N, false);
-  }
-
-  void listTest(int N, bool callDestructor) {
-    CDChunkList<int> list(d_context, callDestructor,
-                          ContextMemoryAllocator<int>(d_context->getCMM()));
-
-    TS_ASSERT(list.empty());
-    for (int i = 0; i < N; ++i) {
-      TS_ASSERT_EQUALS(list.size(), unsigned(i));
-      list.push_back(i);
-      TS_ASSERT(!list.empty());
-      TS_ASSERT_EQUALS(list.back(), i);
-      int i2 = 0;
-      for (CDChunkList<int>::const_iterator j = list.begin(); j != list.end();
-           ++j) {
-        TS_ASSERT_EQUALS(*j, i2++);
-      }
-    }
-    TS_ASSERT_EQUALS(list.size(), unsigned(N));
-
-    for (int i = 0; i < N; ++i) {
-      TS_ASSERT_EQUALS(list[i], i);
-    }
-  }
-
-  void testEmptyIterator() {
-    CDChunkList<int>* list = new (d_context->getCMM())
-        CDChunkList<int>(true, d_context, false,
-                         ContextMemoryAllocator<int>(d_context->getCMM()));
-    TS_ASSERT_EQUALS(list->begin(), list->end());
-  }
-
-  void testDtorCalled() {
-    bool shouldRemainFalse = false;
-    bool shouldFlipToTrue = false;
-    bool alsoFlipToTrue = false;
-    bool shouldAlsoRemainFalse = false;
-    bool aThirdFalse = false;
-
-    CDChunkList<DtorSensitiveObject> listT(
-        d_context, true,
-        ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
-    CDChunkList<DtorSensitiveObject> listF(
-        d_context, false,
-        ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
-
-    DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse);
-    DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue);
-    DtorSensitiveObject alsoFlipToTrueDSO(alsoFlipToTrue);
-    DtorSensitiveObject shouldAlsoRemainFalseDSO(shouldAlsoRemainFalse);
-    DtorSensitiveObject aThirdFalseDSO(aThirdFalse);
-
-    listT.push_back(shouldAlsoRemainFalseDSO);
-    listF.push_back(shouldAlsoRemainFalseDSO);
-
-    d_context->push();
-
-    listT.push_back(shouldFlipToTrueDSO);
-    listT.push_back(alsoFlipToTrueDSO);
-
-    listF.push_back(shouldRemainFalseDSO);
-    listF.push_back(shouldAlsoRemainFalseDSO);
-    listF.push_back(aThirdFalseDSO);
-
-    TS_ASSERT_EQUALS(shouldRemainFalse, false);
-    TS_ASSERT_EQUALS(shouldFlipToTrue, false);
-    TS_ASSERT_EQUALS(alsoFlipToTrue, false);
-    TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false);
-    TS_ASSERT_EQUALS(aThirdFalse, false);
-
-    d_context->pop();
-
-    TS_ASSERT_EQUALS(shouldRemainFalse, false);
-    TS_ASSERT_EQUALS(shouldFlipToTrue, true);
-    TS_ASSERT_EQUALS(alsoFlipToTrue, true);
-    TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false);
-    TS_ASSERT_EQUALS(aThirdFalse, false);
-  }
-
-  void testOutOfMemory() {
-#ifdef CVC4_MEMORY_LIMITING_DISABLED
-
-    CVC4::test::WarnWithLimitedMemoryDisabledReason();
-
-#else /* CVC4_MEMORY_LIMITING_DISABLED */
-
-    CDChunkList<unsigned> list(d_context);
-    CVC4::test::WithLimitedMemory wlm(1);
-
-    TS_ASSERT_THROWS(
-        {
-          // We cap it at UINT_MAX, preferring to terminate with a
-          // failure than run indefinitely.
-          for (unsigned i = 0; i < UINT_MAX; ++i) {
-            list.push_back(i);
-          }
-        },
-        bad_alloc);
-
-#endif /* CVC4_MEMORY_LIMITING_DISABLED */
-  }
-};