Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 2578d0b7f..d7b66d52d 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -55,6 +55,8 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
 option elimTautQuant --elim-taut-quant bool :default true
  eliminate tautological disjuncts of quantified formulas
+option purifyQuant --purify-quant bool :default false
+ purify quantified formulas
  
 #### E-matching options
  
@@ -241,7 +243,7 @@ option cbqiSat --cbqi-sat bool :read-write :default true
  answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
 option cbqiModel --cbqi-model bool :read-write :default true
  guide instantiations by model values for counterexample-based quantifier instantiation
-option cbqiAll --cbqi-all bool :default false
+option cbqiAll --cbqi-all bool :read-write :default false
  apply counterexample-based instantiation to all quantified formulas
 option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
  use integer infinity for vts in counterexample-based quantifier instantiation