fix(CMakeLists.txt): GCC 9.1.0 miscompiles certain if statements #63

src/CMakeLists.txt

@@ -242,6 +242,10 @@ if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
         COMMAND "${CMAKE_CXX_COMPILER}" -dumpversion OUTPUT_VARIABLE GCC_VERSION)
     if (NOT (GCC_VERSION VERSION_GREATER 4.9 OR GCC_VERSION VERSION_EQUAL 4.9))
         message(FATAL_ERROR "${PROJECT_NAME} requires g++ 4.9 or greater.")
+    # TODO(Vtec234): Add upper bound when GCC with a fix is released
+    elseif (GCC_VERSION VERSION_GREATER 9.1 OR GCC_VERSION VERSION_EQUAL 9.1)
+        # Work around https://gcc.gnu.org/bugzilla/show_bug.cgi?id=91597
+        set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdisable-tree-ifcombine")
     endif ()
 elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
   set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D__CLANG__")

src/kernel/expr_maps.h

@@ -23,4 +23,4 @@ class expr_cond_bi_map : public std::unordered_map<expr, T, expr_hash, is_cond_b
     expr_cond_bi_map(bool use_bi = false):
         std::unordered_map<expr, T, expr_hash, is_cond_bi_equal_proc>(10, expr_hash(), is_cond_bi_equal_proc(use_bi)) {}
 };
-};
+}

src/library/arith_instance.h

@@ -141,4 +141,4 @@ class arith_instance {
 
     optional<mpq> eval(expr const & e);
 };
-};
+}

src/util/log_tree.cpp

@@ -49,11 +49,11 @@ void log_tree::node::for_each(std::function<bool(log_tree::node const &)> const
             c.for_each(fn);
         });
     }
-};
+}
 
 void log_tree::for_each(std::function<bool(log_tree::node const &)> const & fn) const { // NOLINT
     m_root.for_each(fn);
-};
+}
 
 void log_tree::node::detach_core(std::vector<log_tree::event> & events) const {
     if (m_ptr->m_detached) return;

src/util/numerics/double.cpp

@@ -21,4 +21,4 @@ double numeric_traits<double>::g_one = 1.0;
 double numeric_traits<double>::log(double d) {
     return std::log(d);
 }
-};
+}

src/util/numerics/float.cpp

@@ -24,4 +24,4 @@ static float g_one = 1.0;
 float const & numeric_traits<float>::one() {
     return g_one;
 }
-};
+}

src/util/numerics/numeric_traits.cpp

@@ -17,4 +17,4 @@ void set_processor_rounding(bool plus_inf) {
     else
         std::fesetround(FE_DOWNWARD);
 }
-};
+}

src/util/task_builder.h

@@ -135,7 +135,7 @@ class task_builder {
 template <class Res, class Fn, class Arg>
 task_builder<Res> map(task<Arg> const & arg, Fn && fn) {
     return std::move(task_builder<Res>([arg, fn] { return fn(get(arg)); }).depends_on(arg));
-};
+}
 
 template <class Res>
 task<std::vector<Res>> traverse(std::vector<task<Res>> const & ts) {
@@ -200,6 +200,6 @@ gtask mk_deep_dependency(task<Arg> const & arg, Fn && fn) {
             fn(deps, *v);
         }
     });
-};
+}
 
 }

src/util/thread.h

@@ -15,7 +15,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace chrono = std::chrono;
-};
+}
 
 #if defined(LEAN_MULTI_THREAD)
 #include <thread>