diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index d32e51bf6d5..2ae667eeb13 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -390,8 +390,7 @@ void function_call_harness_generatort::validate_options( "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT}; } - const auto &function_pointer_type = - ns.follow(function_pointer_symbol_pointer->type); + const auto &function_pointer_type = function_pointer_symbol_pointer->type; if(!can_cast_type(function_pointer_type)) {