Add local theory extensions instantiation strategy (incomplete). Refactor how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.

1 files changed, 2 insertions, 0 deletions

diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 011e2924d..7a959a70d 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -150,6 +150,8 @@ private:
   // quantifier/index for the variable we are matching
   Node d_f;
   unsigned d_index;
+  //first time
+  bool d_firstTime;
 public:
   CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
   ~CandidateGeneratorQEAll(){}