calling a FnMut from a closure

[boulme]

Hello,

On this file, I got this error from Creusot:

cargo creusot -- --features=contracts -v
       Fresh autocfg v1.1.0
       Fresh unicode-ident v1.0.12
       Fresh cfg-if v1.0.0
       Fresh proc-macro2 v1.0.69
       Fresh num-traits v0.2.17
       Fresh quote v1.0.33
       Fresh libc v0.2.149
       Fresh num-integer v0.1.45
       Fresh syn v2.0.38
       Fresh getrandom v0.2.10
       Fresh num-bigint v0.3.3
       Fresh creusot-contracts-dummy v0.2.0 (https://github.com/xldenis/creusot.git#3e2e9877)
       Fresh pearlite-syn v0.2.0 (https://github.com/xldenis/creusot.git#3e2e9877)
       Fresh uuid v1.4.1
       Fresh num-rational v0.3.2
       Fresh creusot-contracts-proc v0.2.0 (https://github.com/xldenis/creusot.git#3e2e9877)
       Fresh creusot-contracts v0.2.0 (https://github.com/xldenis/creusot.git#3e2e9877)
       Dirty essai_creusot v0.1.0 (/home/boulme/RECH/CompilingRust/essai_creusot): the file `src/main.rs` has changed (1696970426.021343186s, 1m 58s after last build at 1696970308.682210561s)
    Checking essai_creusot v0.1.0 (/home/boulme/RECH/CompilingRust/essai_creusot)
     Running `/home/boulme/.cargo/bin/creusot-rustc /home/boulme/.rustup/toolchains/nightly-2023-06-29-x86_64-unknown-linux-gnu/bin/rustc --crate-name essai_creusot --edition=2021 src/main.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=181 --crate-type bin --emit=dep-info,metadata -C embed-bitcode=no -C debuginfo=2 --cfg 'feature="contracts"' -C metadata=61b1bb465d0330f2 -C extra-filename=-61b1bb465d0330f2 --out-dir /home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps -C incremental=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/incremental -L dependency=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps --extern creusot_contracts=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps/libcreusot_contracts-f0c7b7209bf7c69c.rmeta`
warning: unused import: `logic::Int`
 --> src/main.rs:5:25
  |
5 | use creusot_contracts::{logic::Int, *};
  |                         ^^^^^^^^^^
  |
  = note: `#[warn(unused_imports)]` on by default

thread 'rustc' panicked at 'internal error: entered unreachable code', creusot/src/backend/clone_map.rs:884:14
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

note: Creusot has panic-ed!
  |
  = note: Oops, that shouldn't have happened, sorry about that.
  = note: Please report this bug over here: https://github.com/xldenis/creusot/issues/new

warning: `essai_creusot` (bin "essai_creusot") generated 1 warning (run `cargo fix --bin "essai_creusot"` to apply 1 suggestion)
error: could not compile `essai_creusot` (bin "essai_creusot"); 1 warning emitted

Caused by:
  process didn't exit successfully: `/home/boulme/.cargo/bin/creusot-rustc /home/boulme/.rustup/toolchains/nightly-2023-06-29-x86_64-unknown-linux-gnu/bin/rustc --crate-name essai_creusot --edition=2021 src/main.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=181 --crate-type bin --emit=dep-info,metadata -C embed-bitcode=no -C debuginfo=2 --cfg 'feature="contracts"' -C metadata=61b1bb465d0330f2 -C extra-filename=-61b1bb465d0330f2 --out-dir /home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps -C incremental=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/incremental -L dependency=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps --extern creusot_contracts=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps/libcreusot_contracts-f0c7b7209bf7c69c.rmeta` (exit status: 101)

[xldenis]

Oh wow, that's a deep and nasty panic, I actually think this won't be hard to fix, it seems like we are just forgetting to handle closures in one case statement 🤞 .

[arnaudgolfouse]

I think this was resolved ? I cannot reproduce it on the latest creusot version.

[xldenis]

Hmm if you can't reproduce I suppose we can consider this closed, it was likely fixed as a side-effect of the CloneMap rewrites.