tests/genmc/fail/shims/mutex_diff_thread_unlock.stderr

Running GenMC Verification...
error: Undefined Behavior: Invalid unlock() operation
  --> RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
   |
LL |             self.lock.inner.unlock();
   |             ^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
   |
   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
   = note: this is on thread `unnamed-ID`
   = note: stack backtrace:
           0: <std::sync::MutexGuard<'_, u64> as std::ops::Drop>::drop
               at RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
           1: std::ptr::drop_in_place))
               at RUSTLIB/core/src/ptr/mod.rs:LL:CC
           2: std::ptr::drop_in_place))
               at RUSTLIB/core/src/ptr/mod.rs:LL:CC
           3: std::mem::drop
               at RUSTLIB/core/src/mem/mod.rs:LL:CC
           4: miri_start::{closure#0}
               at tests/genmc/fail/shims/mutex_diff_thread_unlock.rs:LL:CC
note: the last function in that backtrace got called indirectly due to this code
  --> tests/genmc/fail/shims/mutex_diff_thread_unlock.rs:LL:CC
   |
LL |       let handle = std::thread::spawn(move || {
   |  __________________^
LL | |         let guard = guard; // avoid field capturing
LL | |         drop(guard);
LL | |     });
   | |______^

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report

error: aborting due to 1 previous error