Minor changes to smt comp script for quantified arith. Add option --cbqi-sat whether to disable sat for quantified arith.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 21056bc05..dc5b976f0 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -87,6 +87,8 @@ private:
   bool doCbqi( Node f );
   /** is the engine incomplete for this quantifier */
   bool isIncomplete( Node f );
+  /** cbqi set inactive */
+  bool d_cbqi_set_quant_inactive;
 private:
   /** do instantiation round */
   bool doInstantiationRound( Theory::Effort effort );
@@ -98,7 +100,7 @@ public:
   /** initialize */
   void finishInit();
 
-  bool needsCheck( Theory::Effort e ); 
+  bool needsCheck( Theory::Effort e );
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();