Significant work on bug #491 (not yet closed).

1 files changed, 5 insertions, 1 deletions

diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 31a6b9141..a199256e7 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -62,6 +62,9 @@ private:
   /** Cache of the already performed substitutions */
   NodeCache d_substitutionCache;
 
+  /** Whether or not to substitute under quantifiers */
+  bool d_substituteUnderQuantifiers;
+
   /** Has the cache been invalidated? */
   bool d_cacheInvalidated;
 
@@ -95,10 +98,11 @@ private:
 
 public:
 
-  SubstitutionMap(context::Context* context) :
+  SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true) :
     d_context(context),
     d_substitutions(context),
     d_substitutionCache(),
+    d_substituteUnderQuantifiers(substituteUnderQuantifiers),
     d_cacheInvalidated(false),
     d_cacheInvalidator(context, d_cacheInvalidated) {
   }