diff options
| -rw-r--r-- | src/theory/type_enumerator.h | 18 |
1 files 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; } |