Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement to performance of E-matching.

1 files changed, 5 insertions, 1 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 577fa7413..c59d87d40 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1358,7 +1358,11 @@ void SmtEngine::setDefaults() {
       options::finiteModelFind.set( true );
     }
   }
-
+  if( options::finiteModelFind() ){
+    if( !options::quantConflictFind.wasSetByUser() ){
+      options::quantConflictFind.set( false );
+    }
+  }
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
     if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){