diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index c758f2942afa..2827f058c3a2 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -791,7 +791,7 @@ impl GotocCtx<'_, '_> {
                 Stmt::block(
                     vec![
                         self.codegen_expr_to_place_stable(destination, func_expr.call(fargs), loc),
-                        Stmt::goto(bb_label(target.unwrap()), loc),
+                        self.codegen_end_call(*target, loc),
                     ],
                     loc,
                 )
diff --git a/tests/kani/Never/fn_ptr_never_return.rs b/tests/kani/Never/fn_ptr_never_return.rs
new file mode 100644
index 000000000000..4670a7a03bf2
--- /dev/null
+++ b/tests/kani/Never/fn_ptr_never_return.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+//! Regression test for https://github.com/model-checking/kani/issues/4577
+//!
+//! Calling a function pointer whose return type is the never type `!` used to
+//! panic the Kani compiler in `codegen_funcall`: the function-pointer path
+//! unconditionally unwrapped the call's return target, but a diverging call
+//! has no return target. Codegen must instead treat the missing target like a
+//! direct call to a never-returning function does. Here the callee panics, so
+//! verification reaches the panic and fails (rather than the compiler crashing).
+
+fn diverge() -> ! {
+    panic!("EXPECTED FAIL: diverging function was called");
+}
+
+#[kani::proof]
+fn check_fnptr_never() {
+    let f: fn() -> ! = diverge;
+    f();
+}