Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1ab4ee62a..55e83ee14 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1426,6 +1426,12 @@ void SmtEngine::setDefaults() {
   }
 
   //cbqi options
+  // enable if pure arithmetic quantifiers
+  if( d_logic.isQuantified() && d_logic.isPure(THEORY_ARITH) ){
+    if( !options::cbqi.wasSetByUser() && !options::cbqi2.wasSetByUser() ){
+      options::cbqi2.set( true );
+    }
+  }
   if( options::recurseCbqi() || options::cbqi2() ){
     options::cbqi.set( true );
   }