Refactoring of conjecture generator. Determine subgoals are non-canonical based on ground equalities. Add filtering options to options file.

1 files changed, 11 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cd3a7943e..caa757426 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1310,6 +1310,17 @@ void SmtEngine::setDefaults() {
       options::purifyTriggers.set( true );
     }
   }
+  if( options::conjectureNoFilter() ){
+    if( !options::conjectureFilterActiveTerms.wasSetByUser() ){
+      options::conjectureFilterActiveTerms.set( false );
+    }
+    if( !options::conjectureFilterCanonical.wasSetByUser() ){
+      options::conjectureFilterCanonical.set( false );
+    }
+    if( !options::conjectureFilterModel.wasSetByUser() ){
+      options::conjectureFilterModel.set( false );
+    }
+  }
 
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){