Generated new version of UNIMPLEMENTED_FEATURE addressing error on GCC 12

Author: Enrico Steffinlongo

src/util/invariant.h

@@ -529,8 +529,17 @@ CBMC_NORETURN void report_invariant_failure(
 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...)                    \
   EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
 
-#define UNIMPLEMENTED_FEATURE(FEATURE)                                         \
-  INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE))
+#if __GNUC__
+#  define UNIMPLEMENTED_FEATURE(FEATURE)                                       \
+    do                                                                         \
+    {                                                                          \
+      INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE));     \
+      __builtin_unreachable();                                                 \
+    } while(false)
+#else
+#  define UNIMPLEMENTED_FEATURE(FEATURE)                                       \
+    INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE))
+#endif
 
 // Legacy annotations