some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

1 files changed, 9 insertions, 1 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 66c7e4cbc..1d98ce115 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -69,6 +69,7 @@
 #include "theory/arrays/options.h"
 #include "util/sort_inference.h"
 #include "theory/quantifiers/macros.h"
+#include "theory/datatypes/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -977,6 +978,13 @@ void SmtEngine::setLogicInternal() throw() {
       setOption("check-models", SExpr("false"));
     }
   }
+
+  //datatypes theory should assign values to all datatypes terms if logic is quantified
+  if (d_logic.isQuantified() && d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
+    if( !options::dtForceAssignment.wasSetByUser() ){
+      options::dtForceAssignment.set(true);
+    }
+  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
@@ -2253,7 +2261,7 @@ void SmtEnginePrivate::processAssertions() {
         collectSkolems((*pos).first, skolemSet, cache);
         collectSkolems((*pos).second, skolemSet, cache);
       }
-      
+
       // We need to ensure:
       // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
       // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk