diff --git a/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean b/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean
index 796b5d737..e5bf2cff2 100644
--- a/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean
+++ b/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean
@@ -162,7 +162,8 @@ private partial def coreStmtsToGoto
                 .Integer
             CProverGOTO.Expr.symbol name ty
           | [] => CProverGOTO.Expr.symbol "" .Empty
-        let calleeExpr := CProverGOTO.Expr.symbol procName .Empty
+        let calleeExpr := CProverGOTO.Expr.symbol procName
+          (CProverGOTO.Ty.mkCode (argExprs.map (·.type)) lhsExpr.type)
         let callCode := CProverGOTO.Code.functionCall lhsExpr calleeExpr argExprs
         let inst : CProverGOTO.Instruction :=
           { type := .FUNCTION_CALL, code := callCode, locationNum := trans.nextLoc }
diff --git a/Strata/Backends/CBMC/GOTO/InstToJson.lean b/Strata/Backends/CBMC/GOTO/InstToJson.lean
index 357efd36c..eb51ab351 100644
--- a/Strata/Backends/CBMC/GOTO/InstToJson.lean
+++ b/Strata/Backends/CBMC/GOTO/InstToJson.lean
@@ -64,6 +64,19 @@ def tyToJson (ty : Ty) : Json :=
       ("id", "array"),
       ("sub", Json.arr #[tyToJson elemTy])
     ]
+  | { id := .code, subtypes := retTy :: paramTypes, .. } =>
+    let paramSubs := paramTypes.map fun pTy =>
+      Json.mkObj [("namedSub", Json.mkObj [("type", tyToJson pTy)])]
+    Json.mkObj [
+      ("id", "code"),
+      ("namedSub", Json.mkObj [
+        ("parameters", Json.mkObj [("sub", Json.arr paramSubs.toArray)]),
+        ("return_type", tyToJson retTy)])]
+  | { id := .code, .. } => Json.mkObj [
+      ("id", "code"),
+      ("namedSub", Json.mkObj [
+        ("parameters", Json.mkObj [("sub", Json.arr #[])]),
+        ("return_type", Json.mkObj [("id", "empty")])])]
   | _ => Json.mkObj [("id", "unknown")]
 
 /-- Convert `Expr` to JSON format -/
diff --git a/Strata/Backends/CBMC/GOTO/Type.lean b/Strata/Backends/CBMC/GOTO/Type.lean
index 2be696ce7..ba774a452 100644
--- a/Strata/Backends/CBMC/GOTO/Type.lean
+++ b/Strata/Backends/CBMC/GOTO/Type.lean
@@ -74,6 +74,8 @@ inductive Identifier where
   | structTag (name : String)
   /-- Array type with element type -/
   | array
+  /-- Code (function) type -/
+  | code
   deriving Repr, Inhabited, DecidableEq
 
 instance : ToFormat Identifier where
@@ -82,6 +84,7 @@ instance : ToFormat Identifier where
     | .bitVector bv => f!"{bv}"
     | .structTag name => f!"struct_tag({name})"
     | .array => f!"array"
+    | .code => f!"code"
 
 end Ty
 
@@ -181,6 +184,12 @@ def StructTag (name : _root_.String) : Ty :=
 def Array (elemTy : Ty) : Ty :=
   { id := .array, subtypes := [elemTy] }
 
+/-- Code (function) type with parameter types and return type.
+    Used for FUNCTION_CALL callee symbols.
+    Encodes as subtypes = [returnType] ++ paramTypes. -/
+def mkCode (paramTypes : List Ty) (returnType : Ty) : Ty :=
+  { id := .code, subtypes := returnType :: paramTypes }
+
 end Ty
 
 -------------------------------------------------------------------------------