diff --git a/src/analyze.rs b/src/analyze.rs
index fce97595..c4fbc9e8 100644
--- a/src/analyze.rs
+++ b/src/analyze.rs
@@ -585,6 +585,29 @@ impl<'tcx> Analyzer<'tcx> {
         self.basic_blocks.entry(def_id).or_default().insert(bb, def);
     }
 
+    /// Installs the function types of a basic block's parameters.
+    ///
+    /// A block whose parameters are typed from MIR types alone carries an unrefined
+    /// specification for every function-typed parameter. This overwrites those with
+    /// specifications recovered from elsewhere; see
+    /// [`crate::refine::BasicBlockType::set_param_function_ty`].
+    pub fn register_basic_block_param_function_tys(
+        &mut self,
+        def_id: LocalDefId,
+        bb: BasicBlock,
+        tys: impl IntoIterator<Item = (rty::FunctionParamIdx, rty::FunctionType)>,
+    ) {
+        let bb_def = self
+            .basic_blocks
+            .get_mut(&def_id)
+            .unwrap()
+            .get_mut(&bb)
+            .unwrap();
+        for (idx, ty) in tys {
+            bb_def.ty.set_param_function_ty(idx, ty);
+        }
+    }
+
     pub fn register_basic_block_precondition(
         &mut self,
         def_id: LocalDefId,
diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs
index 4ed04196..730571d6 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -816,11 +816,43 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         }
         capture.push_env_state(&self.env);
         let precondition = capture.finish(&self.env);
+        let function_tys = self.inherited_function_tys(bty);
 
+        self.ctx
+            .register_basic_block_param_function_tys(self.local_def_id, bb, function_tys);
         self.ctx
             .register_basic_block_precondition(self.local_def_id, bb, precondition);
     }
 
+    /// Reads the function types the env holds for a goto target's function-typed params.
+    ///
+    /// A function type carries the callee's specification in the type itself rather than
+    /// in a refinement, so a precondition captured from the env cannot bring it along.
+    /// The target's params are typed from their MIR types alone, which leaves that
+    /// specification unrefined, so the types are handed over as they are instead.
+    fn inherited_function_tys(
+        &self,
+        bty: &BasicBlockType,
+    ) -> Vec<(rty::FunctionParamIdx, rty::FunctionType)> {
+        let mut tys = Vec::new();
+        for (param_idx, param_rty) in bty.as_ref().params.iter_enumerated() {
+            // Only a param standing for a local is ever called; an `OuterFnParam` copy of
+            // a function-typed argument exists to name the argument's entry value.
+            let BasicBlockTypeParamKind::Local(local, _) = bty.param_kind(param_idx) else {
+                continue;
+            };
+            if param_rty.ty.as_function().is_none() {
+                continue;
+            }
+            let local_ty = self.env.local_type(local).ty;
+            let ty = local_ty
+                .as_function()
+                .unwrap_or_else(|| panic!("{local:?} is not of a function type in env"));
+            tys.push((param_idx, ty.clone()));
+        }
+        tys
+    }
+
     fn with_assumptions<F, T>(&mut self, assumptions: Vec<impl Into<Assumption>>, callback: F) -> T
     where
         F: FnOnce(&mut Self) -> T,
diff --git a/src/refine/basic_block.rs b/src/refine/basic_block.rs
index e02e1d68..9c6483e4 100644
--- a/src/refine/basic_block.rs
+++ b/src/refine/basic_block.rs
@@ -137,6 +137,21 @@ impl BasicBlockType {
         self.ty.clone()
     }
 
+    /// Replaces the function type of the parameter at `idx`.
+    ///
+    /// A function type spells out the callee's specification in the type itself, and
+    /// [`crate::refine::TypeBuilder`] leaves that specification unrefined when it builds a
+    /// parameter from its MIR type alone. This installs a specification recovered
+    /// elsewhere.
+    pub fn set_param_function_ty(&mut self, idx: rty::FunctionParamIdx, ty: rty::FunctionType) {
+        let param_ty = &mut self.ty.params[idx].ty;
+        assert!(
+            param_ty.as_function().is_some(),
+            "parameter {idx} is not of a function type"
+        );
+        *param_ty = ty.into();
+    }
+
     pub fn set_precondition(&mut self, refinement: rty::Refinement<rty::FunctionParamIdx>) {
         let last_param_idx = self.ty.params.last_index().unwrap();
         self.ty.params.raw.last_mut().unwrap().refinement = refinement.map_var(|v| {
diff --git a/tests/ui/fail/fn_ptr_call_in_branch.rs b/tests/ui/fail/fn_ptr_call_in_branch.rs
new file mode 100644
index 00000000..a6ffde40
--- /dev/null
+++ b/tests/ui/fail/fn_ptr_call_in_branch.rs
@@ -0,0 +1,18 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn add1(x: i64) -> i64 {
+    x + 1
+}
+
+// `add1(0)` is 1 rather than 0.
+#[thrust::callable]
+fn check(c: bool) {
+    let f: fn(i64) -> i64 = add1;
+    if c {
+        let a = f(0);
+        assert!(a == 0);
+    }
+}
+
+fn main() {}
diff --git a/tests/ui/fail/fn_ptr_call_twice.rs b/tests/ui/fail/fn_ptr_call_twice.rs
new file mode 100644
index 00000000..5b1a1067
--- /dev/null
+++ b/tests/ui/fail/fn_ptr_call_twice.rs
@@ -0,0 +1,15 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn incr(m: &mut i64) {
+    *m += 1;
+}
+
+// `x` is incremented twice, so it is 2 rather than 1 here.
+fn main() {
+    let f: fn(&mut i64) = incr;
+    let mut x = 0;
+    f(&mut x);
+    f(&mut x);
+    assert!(x == 1);
+}
diff --git a/tests/ui/fail/fn_ptr_param_call_twice.rs b/tests/ui/fail/fn_ptr_param_call_twice.rs
new file mode 100644
index 00000000..961ffe5e
--- /dev/null
+++ b/tests/ui/fail/fn_ptr_param_call_twice.rs
@@ -0,0 +1,24 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
+#[thrust::trusted]
+fn rand() -> i64 { unimplemented!() }
+
+fn incr(m: &mut i64) {
+    *m += 1;
+}
+
+fn app(f: fn(&mut i64), mut x: i64) -> i64 {
+    f(&mut x);
+    f(&mut x);
+    x
+}
+
+// `x` is incremented twice, so it is `i + 2` rather than `i + 1` here.
+fn main() {
+    let i = rand();
+    let x = app(incr, i);
+    assert!(x == i + 1);
+}
diff --git a/tests/ui/pass/fn_ptr_call_in_branch.rs b/tests/ui/pass/fn_ptr_call_in_branch.rs
new file mode 100644
index 00000000..3dfcc6c2
--- /dev/null
+++ b/tests/ui/pass/fn_ptr_call_in_branch.rs
@@ -0,0 +1,20 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn add1(x: i64) -> i64 {
+    x + 1
+}
+
+// The cast that produces `f` and the call of `f` sit in different basic blocks.
+// The callee's specification must survive that boundary; without it the call's
+// result is unconstrained.
+#[thrust::callable]
+fn check(c: bool) {
+    let f: fn(i64) -> i64 = add1;
+    if c {
+        let a = f(0);
+        assert!(a == 1);
+    }
+}
+
+fn main() {}
diff --git a/tests/ui/pass/fn_ptr_call_twice.rs b/tests/ui/pass/fn_ptr_call_twice.rs
new file mode 100644
index 00000000..2ddce151
--- /dev/null
+++ b/tests/ui/pass/fn_ptr_call_twice.rs
@@ -0,0 +1,17 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn incr(m: &mut i64) {
+    *m += 1;
+}
+
+// A call ends its basic block, so the second call sees `f` re-entering the block
+// it lives in. The callee's specification must survive that boundary; without it
+// the second call's effect on `x` is unconstrained.
+fn main() {
+    let f: fn(&mut i64) = incr;
+    let mut x = 0;
+    f(&mut x);
+    f(&mut x);
+    assert!(x == 2);
+}
diff --git a/tests/ui/pass/fn_ptr_param_call_twice.rs b/tests/ui/pass/fn_ptr_param_call_twice.rs
new file mode 100644
index 00000000..4cbde632
--- /dev/null
+++ b/tests/ui/pass/fn_ptr_param_call_twice.rs
@@ -0,0 +1,26 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
+#[thrust::trusted]
+fn rand() -> i64 { unimplemented!() }
+
+fn incr(m: &mut i64) {
+    *m += 1;
+}
+
+// A call ends its basic block, so the second call sees `f` re-entering the block
+// it lives in. The specification the caller supplied for `f` must survive that
+// boundary; without it the second call's effect on `x` is unconstrained.
+fn app(f: fn(&mut i64), mut x: i64) -> i64 {
+    f(&mut x);
+    f(&mut x);
+    x
+}
+
+fn main() {
+    let i = rand();
+    let x = app(incr, i);
+    assert!(x == i + 2);
+}