disable model-generation by default in cvc3 compatibility layer. should fix system...

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 95417845f4048bc56cff2a0a01d97dcfca7cceca..8ba91b41944bab59b693a99d42915039edf37afd 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -738,7 +738,9 @@ void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflag
   // always incremental and model-producing in CVC3 compatibility mode
   // also incrementally-simplifying and interactive
   d_smt->setOption("incremental", string("true"));
-  d_smt->setOption("produce-models", string("true"));
+  // disable this option by default for now, because datatype models
+  // are broken [MGD 10/4/2012]
+  //d_smt->setOption("produce-models", string("true"));
   d_smt->setOption("simplification-mode", string("incremental"));
   d_smt->setOption("interactive-mode", string("true"));// support SmtEngine::getAssertions()
 

diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 8c56b8f3f1f0bd482d4dd67f42fe051545b70e2b..0db2ea89194e7e92b02238e9c785368915e46adc 100644 (file)
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -19,8 +19,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__MODEs_H
-#define __CVC4__THEORY__QUANTIFIERS__MODEs_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__MODES_H
+#define __CVC4__THEORY__QUANTIFIERS__MODES_H
 
 #include <iostream>
 
@@ -65,4 +65,4 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mo
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H */
+#endif /* __CVC4__THEORY__QUANTIFIERS__MODES_H */