Merge quantifiers2-trunk:

   - new syntax for rewrite rules
   - better rewrite rules theory
   - remove the rewriting with rewrite rules during ppRewrite temporarily
   - theory can define their own candidate generator
   - define a general candidate generator (inefficient ask to every theory)
   - split inst_match between the pattern matching used for quantifiers (inst_match.*) and
     the one used for rewrite rules (rr_inst_match.*):
      - the pattern matching is less exhaustive for quantifiers,
      - the one for rewrite rules can use efficient-e-matching.

2 files changed, 4 insertions, 4 deletions

diff --git a/src/context/cdo.h b/src/context/cdo.h
index 025e8e337..1fc1eebe6 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -59,7 +59,7 @@ protected:
    * using the ContextMemoryManager.
    */
   virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    Debug("context") << "save cdo " << this << " (value " << get() << ")";
+    Debug("context") << "save cdo " << this;
     ContextObj* p = new(pCMM) CDO<T>(*this);
     Debug("context") << " to " << p << std::endl;
     return p;
@@ -70,7 +70,7 @@ protected:
    * saved data back from the saved copy using operator= for T.
    */
   virtual void restore(ContextObj* pContextObj) {
-    //Debug("context") << "restore cdo " << this << " from " << get();
+    //Debug("context") << "restore cdo " << this;
     d_data = ((CDO<T>*) pContextObj)->d_data;
     //Debug("context") << " to " << get() << std::endl;
   }
diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h
index b43217cfe..abdcc0493 100644
--- a/src/context/cdqueue.h
+++ b/src/context/cdqueue.h
@@ -63,7 +63,7 @@ protected:
    *  We assume that the base class do the job inside their copy constructor.
    */
   ContextObj* save(ContextMemoryManager* pCMM) {
-    ContextObj* data = new(pCMM) CDQueue<T>(*this);
+    ContextObj* data = new(pCMM) CDQueue<T, CleanUp, Allocator>(*this);
     // We save the d_size in d_lastsave and we should never destruct below this
     // indices before the corresponding restore.
     d_lastsave = ParentType::d_size;
@@ -83,7 +83,7 @@ protected:
    * the list pointer and the allocated size are not changed.
    */
   void restore(ContextObj* data) {
-    CDQueue<T>* qdata = static_cast<CDQueue<T>*>(data);
+    CDQueue<T, CleanUp, Allocator>* qdata = static_cast<CDQueue<T, CleanUp, Allocator>*>(data);
     d_iter = qdata->d_iter;
     d_lastsave = qdata->d_lastsave;
     ParentType::restore(data);