fix bug 650

diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index 551c0b0ee260fbb3fa597d910fe3cc2e5fdc7f7a..fa8f108c308fe8d6d54336af71c3dae6b8bdd35a 100644 (file)
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -62,6 +62,7 @@ public:
   // by the TypeEnumerator framework.
   SetEnumerator(const SetEnumerator& ae) throw() :
     TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)),
+    d_index(ae.d_index),
     d_constituentType(ae.d_constituentType),
     d_nm(ae.d_nm),
     d_indexVec(ae.d_indexVec),