diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
index 6798ab45032dc0a52adf46377a58d083bd18cbe7..e05182d3e47d195f9b7a4d9f533cc82f7a079c3a 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
@@ -1,4 +1,4 @@
-#!/usr/usr/bin/awk -f
+#!/usr/bin/awk -f
 # SPDX-License-Identifier: GPL-2.0
 
 # Modify SRCU for formal verification. The first argument should be srcu.h and