From 7374f204559ef62a1c23de6b286c8ba3eb3efa5d Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 19 Jun 2013 18:27:42 -0400
Subject: [PATCH] Workaround for suspected clang 3.0 codegen bug on Mac

---
 src/theory/type_enumerator.h | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index 777326a26..467bf1927 100644
--- 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; }
-- 
2.30.2