I think this may be an improvement in GCC's `maybe-uninitialized` check but it means that CPROVER can't be built using GCC 9.0: ``` Complexity_limiter.cpp:101:60 error: '*((void*)& loop_to_blacklist +8)' may be used uninitialized in this function [-Werror=maybe-uninitialized] ``` @johndumbell : I think this is your code and a glance does suggest it is possible that `loops_to_blacklist` does not get modified before it is returned.