Fix unsoundness: If pre token can not be found, the postcondition (without condition) can be merged with true

src/verify/declaration.rs

@@ -1996,7 +1996,7 @@ fn assume_axioms(ctx: &mut VerifyContext<'_>, program: &vmir::Program) -> Result
             // `#ensures` occurs only inside a post, which reaches a caller through
             // [`post_fact`] and never through a call — so its token is released by
             // the export instead ([`PostRecipe::token`]).
-            let pre_token = Some(ctx.alloc.fn_pre_token(id, &name));
+            let pre_token = ctx.alloc.fn_pre_token(id, &name);
             ctx.axiom_rules.push(crate::verify::rewrite::function_rule(
                 &name,
                 func,

src/verify/mod.rs

@@ -70,8 +70,9 @@ pub fn verify_with_stats(
     // Verified function bodies, cached in dependency order (callees before
     // callers). Each unit's `assume_axioms` installs one lazy unfold rule per
     // entry here (see `rewrite::function_rule`), which installs the
-    // definitional equality `f(args) == body` the moment a `FuncApp(f, ..)`
-    // occurrence is seen during that unit's own saturation.
+    // definitional equality `f(args) == body` (behind the call's `f%pre(args)`
+    // token) once a called `FuncApp(f, ..)` occurrence is seen during that
+    // unit's own saturation.
     let mut fn_certs: crate::dhash::HashMap<
         vmir::MemberId,
         std::sync::Arc<cert::FunctionDefinition>,