Unpacking is not pure, but could be. The prover panics if you try.

[msaaltink]

public struct S (u8)

#[ext(pure)]
public fun unwrap(s: S): u8 {
    let S(x) = s;
    x
}

public fun f(s: S): u8 {
    s.unwrap() + 1
}

#[spec(prove)]
public fun f_spec(s: S): u8 {
    let s0 = prover::prover::val(&s);
    requires(s0.unwrap() < 255);
    f(s)
}

When running the prover, gets an error:

 'main' (402475) panicked at crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs:3266:29:
unexpected operation Unpack(ModuleId(136), DatatypeId(Symbol(517)), []) in function playground::unwrap