Workaround for suspected clang 3.0 codegen bug on Mac

diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index 777326a267e785f2a0eb319748a95deefef84d38..467bf19274cac54992f5d8a5960119a37a271652 100644 (file)
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -98,7 +98,10 @@ public:
   ~TypeEnumerator() { delete d_te; }
 
   bool isFinished() throw() {
-#ifdef CVC4_ASSERTIONS
+// On Mac clang, there appears to be a code generation bug in an exception
+// block here.  For now, there doesn't appear a good workaround; just disable
+// assertions on that setup.
+#if defined(CVC4_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__))
     if(d_te->isFinished()) {
       try {
         **d_te;
@@ -108,6 +111,8 @@ public:
         //
         // This block can crash on clang 3.0 on Mac OS, perhaps related to
         // bug:  http://llvm.org/bugs/show_bug.cgi?id=13359
+        //
+        // Hence the #if !(defined(__APPLE__) && defined(__clang__)) above
       }
     } else {
       try {
@@ -116,11 +121,14 @@ public:
         Assert(false, "didn't expect a NoMoreValuesException to be thrown");
       }
     }
-#endif /* CVC4_ASSERTIONS */
+#endif /* CVC4_ASSERTIONS && !(APPLE || clang) */
     return d_te->isFinished();
   }
   Node operator*() throw(NoMoreValuesException) {
-#ifdef CVC4_ASSERTIONS
+// On Mac clang, there appears to be a code generation bug in an exception
+// block above (and perhaps here, too).  For now, there doesn't appear a
+// good workaround; just disable assertions on that setup.
+#if defined(CVC4_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__))
     try {
       Node n = **d_te;
       Assert(n.isConst());
@@ -130,9 +138,9 @@ public:
       Assert(isFinished());
       throw;
     }
-#else /* CVC4_ASSERTIONS */
+#else /* CVC4_ASSERTIONS && !(APPLE || clang) */
     return **d_te;
-#endif /* CVC4_ASSERTIONS */
+#endif /* CVC4_ASSERTIONS && !(APPLE || clang) */
   }
   TypeEnumerator& operator++() throw() { ++*d_te; return *this; }
   TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; }