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.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 9228e29d4..0b461131e 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -794,7 +794,7 @@ class EqClassesIterator {
 
 public:
 
-  EqClassesIterator() { }
+  EqClassesIterator(): d_ee(NULL), d_it(0){ }
   EqClassesIterator(eq::EqualityEngine* ee) : d_ee(ee) {
     d_it = 0;
     if ( d_it < d_ee->d_nodesCount &&
@@ -840,7 +840,7 @@ class EqClassIterator {
 
 public:
 
-  EqClassIterator() { }
+  EqClassIterator(): d_ee(NULL){ }
   EqClassIterator(Node eqc, eq::EqualityEngine* ee) : d_ee(ee) {
     Assert( d_ee->getRepresentative(eqc) == eqc );
     d_rep = eqc;