From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 4 Oct 2012 20:48:13 +0000 (+0000)
Subject: disable model-generation by default in cvc3 compatibility layer.  should fix system... 
X-Git-Tag: cvc5-1.0.0~7739
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7a9899f394476e53b7f759e698c7e10c8388fd57;p=cvc5.git

disable model-generation by default in cvc3 compatibility layer.  should fix system test failure (bug 414).
---

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 95417845f..8ba91b419 100644
--- 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 8c56b8f3f..0db2ea891 100644
--- 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 */