[INFO] fetching crate vstd 0.0.0-2026-04-20-1748...
[INFO] testing vstd-0.0.0-2026-04-20-1748 against 1.95.0 for beta-1.96-2
[INFO] extracting crate vstd 0.0.0-2026-04-20-1748 into /workspace/builds/worker-5-tc1/source
[INFO] started tweaking crates.io crate vstd 0.0.0-2026-04-20-1748
[INFO] finished tweaking crates.io crate vstd 0.0.0-2026-04-20-1748
[INFO] tweaked toml for crates.io crate vstd 0.0.0-2026-04-20-1748 written to /workspace/builds/worker-5-tc1/source/Cargo.toml
[INFO] validating manifest of crates.io crate vstd 0.0.0-2026-04-20-1748 on toolchain 1.95.0
[INFO] running `Command { std: CARGO_HOME="/workspace/cargo-home" RUSTUP_HOME="/workspace/rustup-home" "/workspace/cargo-home/bin/cargo" "+1.95.0" "metadata" "--manifest-path" "Cargo.toml" "--no-deps", kill_on_drop: false }`
[INFO] crate crates.io crate vstd 0.0.0-2026-04-20-1748 already has a lockfile, it will not be regenerated
[INFO] running `Command { std: CARGO_HOME="/workspace/cargo-home" RUSTUP_HOME="/workspace/rustup-home" "/workspace/cargo-home/bin/cargo" "+1.95.0" "fetch" "--manifest-path" "Cargo.toml", kill_on_drop: false }`
[INFO] [stderr]     Updating crates.io index
[INFO] [stderr]  Downloading crates ...
[INFO] [stderr]   Downloaded verus_builtin v0.0.0-2026-04-12-0118
[INFO] [stderr]   Downloaded verus_builtin_macros v0.0.0-2026-04-20-1748
[INFO] [stderr]   Downloaded verus_prettyplease v0.0.0-2026-04-12-0118
[INFO] [stderr]   Downloaded verus_state_machines_macros v0.0.0-2026-04-20-1748
[INFO] [stderr]   Downloaded verus_syn v0.0.0-2026-04-05-0114
[INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-5-tc1/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-5-tc1/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--user" "0:0" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:d429b63d4308055ea97f60fb1d3dfca48854a00942f1bd2ad806beaf015945ec" "/opt/rustwide/cargo-home/bin/cargo" "+1.95.0" "metadata" "--no-deps" "--format-version=1", kill_on_drop: false }`
[INFO] [stdout] 714e588a9d1ac6c779fa08ad756e8526423611781fc544004075e1e891e34d53
[INFO] running `Command { std: "docker" "start" "-a" "714e588a9d1ac6c779fa08ad756e8526423611781fc544004075e1e891e34d53", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "inspect" "714e588a9d1ac6c779fa08ad756e8526423611781fc544004075e1e891e34d53", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "rm" "-f" "714e588a9d1ac6c779fa08ad756e8526423611781fc544004075e1e891e34d53", kill_on_drop: false }`
[INFO] [stdout] 714e588a9d1ac6c779fa08ad756e8526423611781fc544004075e1e891e34d53
[INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-5-tc1/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-5-tc1/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_INCREMENTAL=0" "-e" "RUST_BACKTRACE=full" "-e" "RUSTFLAGS=--cap-lints=warn" "-e" "RUSTDOCFLAGS=--cap-lints=warn" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--user" "0:0" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:d429b63d4308055ea97f60fb1d3dfca48854a00942f1bd2ad806beaf015945ec" "/opt/rustwide/cargo-home/bin/cargo" "+1.95.0" "build" "--frozen" "--message-format=json", kill_on_drop: false }`
[INFO] [stdout] 166355f7b1b8574285e1677c3097f5777518fe488af35ce0b97b8739b79eae6b
[INFO] running `Command { std: "docker" "start" "-a" "166355f7b1b8574285e1677c3097f5777518fe488af35ce0b97b8739b79eae6b", kill_on_drop: false }`
[INFO] [stderr]    Compiling verus_prettyplease v0.0.0-2026-04-12-0118
[INFO] [stderr]    Compiling vstd v0.0.0-2026-04-20-1748 (/opt/rustwide/workdir)
[INFO] [stderr]    Compiling verus_builtin v0.0.0-2026-04-12-0118
[INFO] [stderr]    Compiling proc-macro2 v1.0.106
[INFO] [stderr]    Compiling indexmap v1.9.3
[INFO] [stderr]    Compiling quote v1.0.45
[INFO] [stderr]    Compiling verus_syn v0.0.0-2026-04-05-0114
[INFO] [stderr]    Compiling syn v2.0.117
[INFO] [stderr]    Compiling synstructure v0.13.2
[INFO] [stderr]    Compiling verus_state_machines_macros v0.0.0-2026-04-20-1748
[INFO] [stderr]    Compiling verus_builtin_macros v0.0.0-2026-04-20-1748
[INFO] [stdout] warning: unused variable: `future`
[INFO] [stdout]   --> future.rs:33:26
[INFO] [stdout]    |
[INFO] [stdout] 33 | fn exec_await<F: Future>(future: F) -> (ret: F::Output)
[INFO] [stdout]    |                          ^^^^^^ help: if this is intentional, prefix it with an underscore: `_future`
[INFO] [stdout]    |
[INFO] [stdout]    = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stderr]     Finished `dev` profile [unoptimized + debuginfo] target(s) in 32.69s
[INFO] running `Command { std: "docker" "inspect" "166355f7b1b8574285e1677c3097f5777518fe488af35ce0b97b8739b79eae6b", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "rm" "-f" "166355f7b1b8574285e1677c3097f5777518fe488af35ce0b97b8739b79eae6b", kill_on_drop: false }`
[INFO] [stdout] 166355f7b1b8574285e1677c3097f5777518fe488af35ce0b97b8739b79eae6b
[INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-5-tc1/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-5-tc1/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_INCREMENTAL=0" "-e" "RUST_BACKTRACE=full" "-e" "RUSTFLAGS=--cap-lints=warn" "-e" "RUSTDOCFLAGS=--cap-lints=warn" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--user" "0:0" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:d429b63d4308055ea97f60fb1d3dfca48854a00942f1bd2ad806beaf015945ec" "/opt/rustwide/cargo-home/bin/cargo" "+1.95.0" "test" "--frozen" "--no-run" "--message-format=json", kill_on_drop: false }`
[INFO] [stdout] 7eea7f41c608440180858373df0133fa097373670c12a25d2457513560c4350b
[INFO] running `Command { std: "docker" "start" "-a" "7eea7f41c608440180858373df0133fa097373670c12a25d2457513560c4350b", kill_on_drop: false }`
[INFO] [stderr]    Compiling vstd v0.0.0-2026-04-20-1748 (/opt/rustwide/workdir)
[INFO] [stdout] warning: unused variable: `future`
[INFO] [stdout]   --> future.rs:33:26
[INFO] [stdout]    |
[INFO] [stdout] 33 | fn exec_await<F: Future>(future: F) -> (ret: F::Output)
[INFO] [stdout]    |                          ^^^^^^ help: if this is intentional, prefix it with an underscore: `_future`
[INFO] [stdout]    |
[INFO] [stdout]    = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] warning: unused variable: `future`
[INFO] [stdout]   --> future.rs:33:26
[INFO] [stdout]    |
[INFO] [stdout] 33 | fn exec_await<F: Future>(future: F) -> (ret: F::Output)
[INFO] [stdout]    |                          ^^^^^^ help: if this is intentional, prefix it with an underscore: `_future`
[INFO] [stdout]    |
[INFO] [stdout]    = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stderr]     Finished `test` profile [unoptimized + debuginfo] target(s) in 3.52s
[INFO] running `Command { std: "docker" "inspect" "7eea7f41c608440180858373df0133fa097373670c12a25d2457513560c4350b", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "rm" "-f" "7eea7f41c608440180858373df0133fa097373670c12a25d2457513560c4350b", kill_on_drop: false }`
[INFO] [stdout] 7eea7f41c608440180858373df0133fa097373670c12a25d2457513560c4350b
[INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-5-tc1/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-5-tc1/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_INCREMENTAL=0" "-e" "RUST_BACKTRACE=full" "-e" "RUSTFLAGS=--cap-lints=warn" "-e" "RUSTDOCFLAGS=--cap-lints=warn" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--user" "0:0" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:d429b63d4308055ea97f60fb1d3dfca48854a00942f1bd2ad806beaf015945ec" "/opt/rustwide/cargo-home/bin/cargo" "+1.95.0" "test" "--frozen", kill_on_drop: false }`
[INFO] [stdout] 656c39cefc06b917a49322ef4f2ef0d3279222d90305047af30ea97622cb70da
[INFO] running `Command { std: "docker" "start" "-a" "656c39cefc06b917a49322ef4f2ef0d3279222d90305047af30ea97622cb70da", kill_on_drop: false }`
[INFO] [stderr] warning: unused variable: `future`
[INFO] [stderr]   --> future.rs:33:26
[INFO] [stderr]    |
[INFO] [stderr] 33 | fn exec_await<F: Future>(future: F) -> (ret: F::Output)
[INFO] [stderr]    |                          ^^^^^^ help: if this is intentional, prefix it with an underscore: `_future`
[INFO] [stderr]    |
[INFO] [stderr]    = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default
[INFO] [stderr] 
[INFO] [stderr] warning: `vstd` (lib) generated 1 warning (run `cargo fix --lib -p vstd` to apply 1 suggestion)
[INFO] [stderr] warning: `vstd` (lib test) generated 1 warning (1 duplicate)
[INFO] [stderr]     Finished `test` profile [unoptimized + debuginfo] target(s) in 0.06s
[INFO] [stderr]      Running unittests vstd.rs (/opt/rustwide/target/debug/deps/vstd-f8549463b3ac992b)
[INFO] [stdout] 
[INFO] [stdout] running 0 tests
[INFO] [stdout] 
[INFO] [stdout] test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s
[INFO] [stdout] 
[INFO] [stderr]    Doc-tests vstd
[INFO] [stdout] 
[INFO] [stdout] running 36 tests
[INFO] [stdout] test cell/invcell.rs - cell::invcell::InvCell (line 23) ... ignored
[INFO] [stdout] test cell/invcell.rs - cell::invcell::InvCell (line 45) ... ignored
[INFO] [stdout] test cell/pcell.rs - cell::pcell::PCell (line 55) ... ignored
[INFO] [stdout] test cell/pcell_maybe_uninit.rs - cell::pcell_maybe_uninit::PCell (line 21) ... ignored
[INFO] [stdout] test arithmetic/overflow.rs - arithmetic::overflow (line 13) ... FAILED
[INFO] [stdout] test invariant.rs - invariant::open_local_invariant (line 462) ... FAILED
[INFO] [stdout] test calc_macro.rs - calc_macro::calc (line 17) ... FAILED
[INFO] [stdout] test atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 299) ... FAILED
[INFO] [stdout] test invariant.rs - invariant::open_local_invariant (line 483) ... FAILED
[INFO] [stdout] test invariant.rs - invariant::open_atomic_invariant (line 355) ... FAILED
[INFO] [stdout] test atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 230) ... FAILED
[INFO] [stdout] test calc_macro.rs - calc_macro::calc (line 37) ... FAILED
[INFO] [stdout] test invariant.rs - invariant::open_local_invariant (line 508) ... FAILED
[INFO] [stdout] test rwlock.rs - rwlock::RwLock (line 278) ... ignored
[INFO] [stdout] test rwlock.rs - rwlock::RwLock (line 309) ... ignored
[INFO] [stdout] test pervasive.rs - pervasive::assert_by_contradiction (line 225) ... FAILED
[INFO] [stdout] test map.rs - map::assert_maps_equal (line 355) ... FAILED
[INFO] [stdout] test pervasive.rs - pervasive::struct_with_invariants (line 306) ... FAILED
[INFO] [stdout] test map.rs - map::assert_maps_equal (line 368) ... FAILED
[INFO] [stdout] test seq_lib.rs - seq_lib::assert_seqs_equal (line 3576) ... FAILED
[INFO] [stdout] test seq_lib.rs - seq_lib::assert_seqs_equal (line 3557) ... FAILED
[INFO] [stdout] test invariant.rs - invariant::open_local_invariant (line 499) ... FAILED
[INFO] [stdout] test pervasive.rs - pervasive::struct_with_invariants (line 276) ... FAILED
[INFO] [stdout] test seq.rs - seq::seq (line 541) ... FAILED
[INFO] [stdout] test set_lib.rs - set_lib::assert_sets_equal (line 1505) ... FAILED
[INFO] [stdout] test thread.rs - thread::spawn (line 68) ... ignored
[INFO] [stdout] test simple_pptr.rs - simple_pptr::PPtr (line 92) ... FAILED
[INFO] [stdout] test set_lib.rs - set_lib::assert_sets_equal (line 1511) ... FAILED
[INFO] [stdout] test raw_ptr.rs - raw_ptr::PointsTo (line 110) ... ok
[INFO] [stdout] test simple_pptr.rs - simple_pptr::PPtr (line 118) ... FAILED
[INFO] [stdout] test tokens/map.rs - tokens::map (line 19) ... FAILED
[INFO] [stdout] test tokens/frac.rs - tokens::frac::FracGhost (line 86) ... FAILED
[INFO] [stdout] test simple_pptr.rs - simple_pptr::PPtr (line 58) ... FAILED
[INFO] [stdout] test tokens/seq.rs - tokens::seq::GhostSeqAuth (line 23) ... FAILED
[INFO] [stdout] test tokens/set.rs - tokens::set (line 20) ... FAILED
[INFO] [stdout] test tokens/frac.rs - tokens::frac::GhostVarAuth (line 335) ... FAILED
[INFO] [stdout] 
[INFO] [stdout] failures:
[INFO] [stdout] 
[INFO] [stdout] ---- arithmetic/overflow.rs - arithmetic::overflow (line 13) stdout ----
[INFO] [stdout] error: expected one of `!`, `(`, `)`, `+`, `,`, `::`, or `<`, found `:`
[INFO] [stdout]   --> arithmetic/overflow.rs:27:47
[INFO] [stdout]    |
[INFO] [stdout] 27 | fn test2(a: u64, b: u64, c: u64, d: u64) -> (e: Option<u64>)
[INFO] [stdout]    |                                               ^ expected one of 7 possible tokens
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- invariant.rs - invariant::open_local_invariant (line 462) stdout ----
[INFO] [stdout] error: expected expression, found `$`
[INFO] [stdout]    --> invariant.rs:463:22
[INFO] [stdout]     |
[INFO] [stdout] 463 | open_local_invariant($inv => $id => {
[INFO] [stdout]     |                      ^ expected expression
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- calc_macro.rs - calc_macro::calc (line 17) stdout ----
[INFO] [stdout] error: cannot find macro `calc` in this scope
[INFO] [stdout]   --> calc_macro.rs:18:1
[INFO] [stdout]    |
[INFO] [stdout] 18 | calc! {
[INFO] [stdout]    | ^^^^
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 299) stdout ----
[INFO] [stdout] error: cannot find macro `atomic_with_ghost` in this scope
[INFO] [stdout]    --> atomic_ghost.rs:300:14
[INFO] [stdout]     |
[INFO] [stdout] 300 | let result = atomic_with_ghost!(
[INFO] [stdout]     |              ^^^^^^^^^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- invariant.rs - invariant::open_local_invariant (line 483) stdout ----
[INFO] [stdout] error: expected pattern, found `$`
[INFO] [stdout]    --> invariant.rs:485:9
[INFO] [stdout]     |
[INFO] [stdout] 485 |     let $id: V = /* an arbitrary value */;
[INFO] [stdout]     |         ^ expected pattern
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- invariant.rs - invariant::open_atomic_invariant (line 355) stdout ----
[INFO] [stdout] error: expected expression, found `$`
[INFO] [stdout]    --> invariant.rs:356:23
[INFO] [stdout]     |
[INFO] [stdout] 356 | open_atomic_invariant($inv => $id => {
[INFO] [stdout]     |                       ^ expected expression
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 230) stdout ----
[INFO] [stdout] error: cannot find macro `atomic_with_ghost` in this scope
[INFO] [stdout]    --> atomic_ghost.rs:231:14
[INFO] [stdout]     |
[INFO] [stdout] 231 | let result = atomic_with_ghost!(
[INFO] [stdout]     |              ^^^^^^^^^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- calc_macro.rs - calc_macro::calc (line 37) stdout ----
[INFO] [stdout] error: cannot find macro `calc` in this scope
[INFO] [stdout]   --> calc_macro.rs:40:1
[INFO] [stdout]    |
[INFO] [stdout] 40 | calc! {
[INFO] [stdout]    | ^^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]   --> calc_macro.rs:38:8
[INFO] [stdout]    |
[INFO] [stdout] 38 | let x: int = 2;
[INFO] [stdout]    |        ^^^
[INFO] [stdout]    |        |
[INFO] [stdout]    |        not found in this scope
[INFO] [stdout]    |        help: perhaps you intended to use this type: `i32`
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]   --> calc_macro.rs:39:8
[INFO] [stdout]    |
[INFO] [stdout] 39 | let y: int = 5;
[INFO] [stdout]    |        ^^^
[INFO] [stdout]    |        |
[INFO] [stdout]    |        not found in this scope
[INFO] [stdout]    |        help: perhaps you intended to use this type: `i32`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 3 previous errors
[INFO] [stdout] 
[INFO] [stdout] For more information about this error, try `rustc --explain E0425`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- invariant.rs - invariant::open_local_invariant (line 508) stdout ----
[INFO] [stdout] error: mismatched closing delimiter: `}`
[INFO] [stdout]    --> invariant.rs:513:32
[INFO] [stdout]     |
[INFO] [stdout] 511 |   |   open_local_invariant!(&inv => id1 => {
[INFO] [stdout]     |                                            - closing delimiter possibly meant for this
[INFO] [stdout] 512 |   |                           ^ this invariant
[INFO] [stdout] 513 |   |       open_local_invariant!(&inv => id2 => {
[INFO] [stdout]     |                                ^ unclosed delimiter
[INFO] [stdout] ...
[INFO] [stdout] 517 |   |   }
[INFO] [stdout]     |       ^ mismatched closing delimiter
[INFO] [stdout] 
[INFO] [stdout] error: this file contains an unclosed delimiter
[INFO] [stdout]    --> invariant.rs:517:8
[INFO] [stdout]     |
[INFO] [stdout] 511 |   |   open_local_invariant!(&inv => id1 => {
[INFO] [stdout]     |                            - unclosed delimiter
[INFO] [stdout] ...
[INFO] [stdout] 517 |   |   }
[INFO] [stdout]     |        ^
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 2 previous errors
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- pervasive.rs - pervasive::assert_by_contradiction (line 225) stdout ----
[INFO] [stdout] error: cannot find macro `assert_by_contradiction` in this scope
[INFO] [stdout]    --> pervasive.rs:226:1
[INFO] [stdout]     |
[INFO] [stdout] 226 | assert_by_contradiction!(b, {
[INFO] [stdout]     | ^^^^^^^^^^^^^^^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- map.rs - map::assert_maps_equal (line 355) stdout ----
[INFO] [stdout] error: expected one of `!` or `::`, found keyword `fn`
[INFO] [stdout]    --> map.rs:356:7
[INFO] [stdout]     |
[INFO] [stdout] 356 | proof fn insert_remove(m: Map<int, int>, k: int, v: int)
[INFO] [stdout]     |       ^^ expected one of `!` or `::`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- pervasive.rs - pervasive::struct_with_invariants (line 306) stdout ----
[INFO] [stdout] error: expected one of `!` or `::`, found `:`
[INFO] [stdout]    --> pervasive.rs:307:20
[INFO] [stdout]     |
[INFO] [stdout] 307 | BoolPredicateDecl  :=  predicate { $bool_expr }
[INFO] [stdout]     |                    ^ expected one of `!` or `::`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- map.rs - map::assert_maps_equal (line 368) stdout ----
[INFO] [stdout] error: expected one of `!` or `::`, found keyword `fn`
[INFO] [stdout]    --> map.rs:369:7
[INFO] [stdout]     |
[INFO] [stdout] 369 | proof fn bitvector_maps() {
[INFO] [stdout]     |       ^^ expected one of `!` or `::`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- seq_lib.rs - seq_lib::assert_seqs_equal (line 3576) stdout ----
[INFO] [stdout] error: expected one of `!` or `::`, found keyword `fn`
[INFO] [stdout]     --> seq_lib.rs:3577:7
[INFO] [stdout]      |
[INFO] [stdout] 3577 | proof fn bitvector_seqs() {
[INFO] [stdout]      |       ^^ expected one of `!` or `::`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- seq_lib.rs - seq_lib::assert_seqs_equal (line 3557) stdout ----
[INFO] [stdout] error: expected one of `!` or `::`, found keyword `fn`
[INFO] [stdout]     --> seq_lib.rs:3558:7
[INFO] [stdout]      |
[INFO] [stdout] 3558 | proof fn subrange_concat(s: Seq<u64>, i: int) {
[INFO] [stdout]      |       ^^ expected one of `!` or `::`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- invariant.rs - invariant::open_local_invariant (line 499) stdout ----
[INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `=>`
[INFO] [stdout]    --> invariant.rs:500:26
[INFO] [stdout]     |
[INFO] [stdout] 500 | open_local_invariant(inv => id1 => {
[INFO] [stdout]     |                          ^^ expected one of 8 possible tokens
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- pervasive.rs - pervasive::struct_with_invariants (line 276) stdout ----
[INFO] [stdout] error: cannot find macro `struct_with_invariants` in this scope
[INFO] [stdout]    --> pervasive.rs:277:1
[INFO] [stdout]     |
[INFO] [stdout] 277 | struct_with_invariants!{
[INFO] [stdout]     | ^^^^^^^^^^^^^^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- seq.rs - seq::seq (line 541) stdout ----
[INFO] [stdout] error: cannot find macro `seq` in this scope
[INFO] [stdout]    --> seq.rs:542:9
[INFO] [stdout]     |
[INFO] [stdout] 542 | let s = seq![11int, 12, 13];
[INFO] [stdout]     |         ^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: expected function, found macro `assert`
[INFO] [stdout]    --> seq.rs:544:1
[INFO] [stdout]     |
[INFO] [stdout] 544 | assert(s.len() == 3);
[INFO] [stdout]     | ^^^^^^ not a function
[INFO] [stdout]     |
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]     |
[INFO] [stdout] 544 | assert!(s.len() == 3);
[INFO] [stdout]     |       +
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: expected function, found macro `assert`
[INFO] [stdout]    --> seq.rs:545:1
[INFO] [stdout]     |
[INFO] [stdout] 545 | assert(s[0] == 11);
[INFO] [stdout]     | ^^^^^^ not a function
[INFO] [stdout]     |
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]     |
[INFO] [stdout] 545 | assert!(s[0] == 11);
[INFO] [stdout]     |       +
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: expected function, found macro `assert`
[INFO] [stdout]    --> seq.rs:546:1
[INFO] [stdout]     |
[INFO] [stdout] 546 | assert(s[1] == 12);
[INFO] [stdout]     | ^^^^^^ not a function
[INFO] [stdout]     |
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]     |
[INFO] [stdout] 546 | assert!(s[1] == 12);
[INFO] [stdout]     |       +
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: expected function, found macro `assert`
[INFO] [stdout]    --> seq.rs:547:1
[INFO] [stdout]     |
[INFO] [stdout] 547 | assert(s[2] == 13);
[INFO] [stdout]     | ^^^^^^ not a function
[INFO] [stdout]     |
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]     |
[INFO] [stdout] 547 | assert!(s[2] == 13);
[INFO] [stdout]     |       +
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 5 previous errors
[INFO] [stdout] 
[INFO] [stdout] For more information about this error, try `rustc --explain E0423`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- set_lib.rs - set_lib::assert_sets_equal (line 1505) stdout ----
[INFO] [stdout] error: cannot find macro `assert_sets_equal` in this scope
[INFO] [stdout]     --> set_lib.rs:1506:1
[INFO] [stdout]      |
[INFO] [stdout] 1506 | assert_sets_equal!(set1 == set2);
[INFO] [stdout]      | ^^^^^^^^^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- simple_pptr.rs - simple_pptr::PPtr (line 92) stdout ----
[INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]   --> simple_pptr.rs:97:17
[INFO] [stdout]    |
[INFO] [stdout] 97 |         let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();
[INFO] [stdout]    |                 ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `PPtr` in this scope
[INFO] [stdout]   --> simple_pptr.rs:97:43
[INFO] [stdout]    |
[INFO] [stdout] 97 |         let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();
[INFO] [stdout]    |                                           ^^^^ use of undeclared type `PPtr`
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]    --> simple_pptr.rs:100:17
[INFO] [stdout]     |
[INFO] [stdout] 100 |         p.write(Tracked(&mut points_to), 5);
[INFO] [stdout]     |                 ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]    --> simple_pptr.rs:103:24
[INFO] [stdout]     |
[INFO] [stdout] 103 |         let x = p.read(Tracked(&points_to));
[INFO] [stdout]     |                        ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]    --> simple_pptr.rs:106:16
[INFO] [stdout]     |
[INFO] [stdout] 106 |         p.free(Tracked(points_to));                 // `points_to` is moved here
[INFO] [stdout]     |                ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]    --> simple_pptr.rs:109:25
[INFO] [stdout]     |
[INFO] [stdout] 109 |         let x2 = p.read(Tracked(&mut points_to));   // so it can't be used here
[INFO] [stdout]     |                         ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 6 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0425, E0433, E0531.
[INFO] [stdout] For more information about an error, try `rustc --explain E0425`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- set_lib.rs - set_lib::assert_sets_equal (line 1511) stdout ----
[INFO] [stdout] error: cannot find macro `assert_sets_equal` in this scope
[INFO] [stdout]     --> set_lib.rs:1512:1
[INFO] [stdout]      |
[INFO] [stdout] 1512 | assert_sets_equal!(set1 == set2, elem => {
[INFO] [stdout]      | ^^^^^^^^^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- simple_pptr.rs - simple_pptr::PPtr (line 118) stdout ----
[INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]    --> simple_pptr.rs:122:17
[INFO] [stdout]     |
[INFO] [stdout] 122 |         let (p, Tracked(mut perm_p)) = PPtr::<u64>::empty();
[INFO] [stdout]     |                 ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]    --> simple_pptr.rs:125:17
[INFO] [stdout]     |
[INFO] [stdout] 125 |         let (q, Tracked(mut perm_q)) = PPtr::<u64>::empty();
[INFO] [stdout]     |                 ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `PPtr` in this scope
[INFO] [stdout]    --> simple_pptr.rs:122:40
[INFO] [stdout]     |
[INFO] [stdout] 122 |         let (p, Tracked(mut perm_p)) = PPtr::<u64>::empty();
[INFO] [stdout]     |                                        ^^^^ use of undeclared type `PPtr`
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `PPtr` in this scope
[INFO] [stdout]    --> simple_pptr.rs:125:40
[INFO] [stdout]     |
[INFO] [stdout] 125 |         let (q, Tracked(mut perm_q)) = PPtr::<u64>::empty();
[INFO] [stdout]     |                                        ^^^^ use of undeclared type `PPtr`
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]    --> simple_pptr.rs:128:16
[INFO] [stdout]     |
[INFO] [stdout] 128 |         p.free(Tracked(perm_p));
[INFO] [stdout]     |                ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]    --> simple_pptr.rs:131:24
[INFO] [stdout]     |
[INFO] [stdout] 131 |         let x = p.read(Tracked(&mut perm_q));
[INFO] [stdout]     |                        ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 6 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0425, E0433, E0531.
[INFO] [stdout] For more information about an error, try `rustc --explain E0425`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- tokens/map.rs - tokens::map (line 19) stdout ----
[INFO] [stdout] error: expected one of `:`, `;`, `=`, `@`, or `|`, found `sub2`
[INFO] [stdout]   --> tokens/map.rs:24:17
[INFO] [stdout]    |
[INFO] [stdout] 24 |     let tracked sub2 = auth.insert_map(map![4u8 => 4u64, 5u8 => 5u64]);
[INFO] [stdout]    |                 ^^^^ expected one of `:`, `;`, `=`, `@`, or `|`
[INFO] [stdout] 
[INFO] [stdout] error: cannot find macro `map` in this scope
[INFO] [stdout]   --> tokens/map.rs:21:57
[INFO] [stdout]    |
[INFO] [stdout] 21 |     let tracked (mut auth, mut sub) = GhostMapAuth::new(map![1u8 => 1u64, 2u8 => 2u64, 3u8 => 3u64]);
[INFO] [stdout]    |                                                         ^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `tracked` in this scope
[INFO] [stdout]   --> tokens/map.rs:21:9
[INFO] [stdout]    |
[INFO] [stdout] 21 |     let tracked (mut auth, mut sub) = GhostMapAuth::new(map![1u8 => 1u64, 2u8 => 2u64, 3u8 => 3u64]);
[INFO] [stdout]    |         ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `GhostMapAuth` in this scope
[INFO] [stdout]   --> tokens/map.rs:21:39
[INFO] [stdout]    |
[INFO] [stdout] 21 |     let tracked (mut auth, mut sub) = GhostMapAuth::new(map![1u8 => 1u64, 2u8 => 2u64, 3u8 => 3u64]);
[INFO] [stdout]    |                                       ^^^^^^^^^^^^ use of undeclared type `GhostMapAuth`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 4 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0433, E0531.
[INFO] [stdout] For more information about an error, try `rustc --explain E0433`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- tokens/frac.rs - tokens::frac::FracGhost (line 86) stdout ----
[INFO] [stdout] error: expected one of `:`, `;`, `=`, `@`, or `|`, found keyword `mut`
[INFO] [stdout]   --> tokens/frac.rs:88:17
[INFO] [stdout]    |
[INFO] [stdout] 88 |     let tracked mut r = FracGhost::<u64, 3>::new(123);
[INFO] [stdout]    |                 ^^^ expected one of `:`, `;`, `=`, `@`, or `|`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- simple_pptr.rs - simple_pptr::PPtr (line 58) stdout ----
[INFO] [stdout] error: invalid comparison operator `===`
[INFO] [stdout]   --> simple_pptr.rs:65:41
[INFO] [stdout]    |
[INFO] [stdout] 65 |         assert(points_to.mem_contents() === MemContents::Uninit);
[INFO] [stdout]    |                                         ^^^
[INFO] [stdout]    |
[INFO] [stdout] help: `===` is not a valid comparison operator, use `==`
[INFO] [stdout]    |
[INFO] [stdout] 65 -         assert(points_to.mem_contents() === MemContents::Uninit);
[INFO] [stdout] 65 +         assert(points_to.mem_contents() == MemContents::Uninit);
[INFO] [stdout]    |
[INFO] [stdout] 
[INFO] [stdout] error: invalid comparison operator `===`
[INFO] [stdout]   --> simple_pptr.rs:71:41
[INFO] [stdout]    |
[INFO] [stdout] 71 |         assert(points_to.mem_contents() === MemContents::Init(5));
[INFO] [stdout]    |                                         ^^^
[INFO] [stdout]    |
[INFO] [stdout] help: `===` is not a valid comparison operator, use `==`
[INFO] [stdout]    |
[INFO] [stdout] 71 -         assert(points_to.mem_contents() === MemContents::Init(5));
[INFO] [stdout] 71 +         assert(points_to.mem_contents() == MemContents::Init(5));
[INFO] [stdout]    |
[INFO] [stdout] 
[INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]   --> simple_pptr.rs:63:17
[INFO] [stdout]    |
[INFO] [stdout] 63 |         let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();
[INFO] [stdout]    |                 ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `PPtr` in this scope
[INFO] [stdout]   --> simple_pptr.rs:63:43
[INFO] [stdout]    |
[INFO] [stdout] 63 |         let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();
[INFO] [stdout]    |                                           ^^^^ use of undeclared type `PPtr`
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `MemContents` in this scope
[INFO] [stdout]   --> simple_pptr.rs:65:45
[INFO] [stdout]    |
[INFO] [stdout] 65 |         assert(points_to.mem_contents() === MemContents::Uninit);
[INFO] [stdout]    |                                             ^^^^^^^^^^^ use of undeclared type `MemContents`
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: expected function, found macro `assert`
[INFO] [stdout]   --> simple_pptr.rs:65:9
[INFO] [stdout]    |
[INFO] [stdout] 65 |         assert(points_to.mem_contents() === MemContents::Uninit);
[INFO] [stdout]    |         ^^^^^^ not a function
[INFO] [stdout]    |
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]    |
[INFO] [stdout] 65 |         assert!(points_to.mem_contents() === MemContents::Uninit);
[INFO] [stdout]    |               +
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: expected function, found macro `assert`
[INFO] [stdout]   --> simple_pptr.rs:66:9
[INFO] [stdout]    |
[INFO] [stdout] 66 |         assert(points_to.pptr() == p);
[INFO] [stdout]    |         ^^^^^^ not a function
[INFO] [stdout]    |
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]    |
[INFO] [stdout] 66 |         assert!(points_to.pptr() == p);
[INFO] [stdout]    |               +
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]   --> simple_pptr.rs:69:17
[INFO] [stdout]    |
[INFO] [stdout] 69 |         p.write(Tracked(&mut points_to), 5);
[INFO] [stdout]    |                 ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `MemContents` in this scope
[INFO] [stdout]   --> simple_pptr.rs:71:45
[INFO] [stdout]    |
[INFO] [stdout] 71 |         assert(points_to.mem_contents() === MemContents::Init(5));
[INFO] [stdout]    |                                             ^^^^^^^^^^^ use of undeclared type `MemContents`
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: expected function, found macro `assert`
[INFO] [stdout]   --> simple_pptr.rs:71:9
[INFO] [stdout]    |
[INFO] [stdout] 71 |         assert(points_to.mem_contents() === MemContents::Init(5));
[INFO] [stdout]    |         ^^^^^^ not a function
[INFO] [stdout]    |
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]    |
[INFO] [stdout] 71 |         assert!(points_to.mem_contents() === MemContents::Init(5));
[INFO] [stdout]    |               +
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: expected function, found macro `assert`
[INFO] [stdout]   --> simple_pptr.rs:72:9
[INFO] [stdout]    |
[INFO] [stdout] 72 |         assert(points_to.pptr() == p);
[INFO] [stdout]    |         ^^^^^^ not a function
[INFO] [stdout]    |
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]    |
[INFO] [stdout] 72 |         assert!(points_to.pptr() == p);
[INFO] [stdout]    |               +
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]   --> simple_pptr.rs:75:24
[INFO] [stdout]    |
[INFO] [stdout] 75 |         let x = p.read(Tracked(&points_to));
[INFO] [stdout]    |                        ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: expected function, found macro `assert`
[INFO] [stdout]   --> simple_pptr.rs:77:9
[INFO] [stdout]    |
[INFO] [stdout] 77 |         assert(x == 5);
[INFO] [stdout]    |         ^^^^^^ not a function
[INFO] [stdout]    |
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]    |
[INFO] [stdout] 77 |         assert!(x == 5);
[INFO] [stdout]    |               +
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope
[INFO] [stdout]   --> simple_pptr.rs:80:30
[INFO] [stdout]    |
[INFO] [stdout] 80 |         let y = p.into_inner(Tracked(points_to));
[INFO] [stdout]    |                              ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: expected function, found macro `assert`
[INFO] [stdout]   --> simple_pptr.rs:82:9
[INFO] [stdout]    |
[INFO] [stdout] 82 |         assert(y == 5);
[INFO] [stdout]    |         ^^^^^^ not a function
[INFO] [stdout]    |
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]    |
[INFO] [stdout] 82 |         assert!(y == 5);
[INFO] [stdout]    |               +
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 15 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0423, E0425, E0433, E0531.
[INFO] [stdout] For more information about an error, try `rustc --explain E0423`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- tokens/seq.rs - tokens::seq::GhostSeqAuth (line 23) stdout ----
[INFO] [stdout] error: expected one of `:`, `;`, `=`, `@`, or `|`, found `sub2`
[INFO] [stdout]   --> tokens/seq.rs:28:17
[INFO] [stdout]    |
[INFO] [stdout] 28 |     let tracked sub2 = sub.split(3);
[INFO] [stdout]    |                 ^^^^ expected one of `:`, `;`, `=`, `@`, or `|`
[INFO] [stdout] 
[INFO] [stdout] error: cannot find macro `seq` in this scope
[INFO] [stdout]   --> tokens/seq.rs:25:57
[INFO] [stdout]    |
[INFO] [stdout] 25 |     let tracked (mut auth, mut sub) = GhostSeqAuth::new(seq![0u64, 1u64, 2u64, 3u64, 4u64, 5u64], 0);
[INFO] [stdout]    |                                                         ^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `tracked` in this scope
[INFO] [stdout]   --> tokens/seq.rs:25:9
[INFO] [stdout]    |
[INFO] [stdout] 25 |     let tracked (mut auth, mut sub) = GhostSeqAuth::new(seq![0u64, 1u64, 2u64, 3u64, 4u64, 5u64], 0);
[INFO] [stdout]    |         ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `GhostSeqAuth` in this scope
[INFO] [stdout]   --> tokens/seq.rs:25:39
[INFO] [stdout]    |
[INFO] [stdout] 25 |     let tracked (mut auth, mut sub) = GhostSeqAuth::new(seq![0u64, 1u64, 2u64, 3u64, 4u64, 5u64], 0);
[INFO] [stdout]    |                                       ^^^^^^^^^^^^ use of undeclared type `GhostSeqAuth`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 4 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0433, E0531.
[INFO] [stdout] For more information about an error, try `rustc --explain E0433`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- tokens/set.rs - tokens::set (line 20) stdout ----
[INFO] [stdout] error: expected one of `:`, `;`, `=`, `@`, or `|`, found `sub2`
[INFO] [stdout]   --> tokens/set.rs:25:17
[INFO] [stdout]    |
[INFO] [stdout] 25 |     let tracked sub2 = auth.insert_set(set![4u8, 5u8]);
[INFO] [stdout]    |                 ^^^^ expected one of `:`, `;`, `=`, `@`, or `|`
[INFO] [stdout] 
[INFO] [stdout] error: cannot find macro `set` in this scope
[INFO] [stdout]   --> tokens/set.rs:22:57
[INFO] [stdout]    |
[INFO] [stdout] 22 |     let tracked (mut auth, mut sub) = GhostSetAuth::new(set![1u8, 2u8, 3u8]);
[INFO] [stdout]    |                                                         ^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `tracked` in this scope
[INFO] [stdout]   --> tokens/set.rs:22:9
[INFO] [stdout]    |
[INFO] [stdout] 22 |     let tracked (mut auth, mut sub) = GhostSetAuth::new(set![1u8, 2u8, 3u8]);
[INFO] [stdout]    |         ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `GhostSetAuth` in this scope
[INFO] [stdout]   --> tokens/set.rs:22:39
[INFO] [stdout]    |
[INFO] [stdout] 22 |     let tracked (mut auth, mut sub) = GhostSetAuth::new(set![1u8, 2u8, 3u8]);
[INFO] [stdout]    |                                       ^^^^^^^^^^^^ use of undeclared type `GhostSetAuth`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 4 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0433, E0531.
[INFO] [stdout] For more information about an error, try `rustc --explain E0433`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- tokens/frac.rs - tokens::frac::GhostVarAuth (line 335) stdout ----
[INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `@`
[INFO] [stdout]    --> tokens/frac.rs:338:17
[INFO] [stdout]     |
[INFO] [stdout] 338 |     assert(gauth@ == 1);
[INFO] [stdout]     |                 ^ expected one of 8 possible tokens
[INFO] [stdout] 
[INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `@`
[INFO] [stdout]    --> tokens/frac.rs:339:16
[INFO] [stdout]     |
[INFO] [stdout] 339 |     assert(gvar@ == 1);
[INFO] [stdout]     |                ^ expected one of 8 possible tokens
[INFO] [stdout] 
[INFO] [stdout] error: expected one of `,`, `:`, or `}`, found `.`
[INFO] [stdout]    --> tokens/frac.rs:341:14
[INFO] [stdout]     |
[INFO] [stdout] 340 |     proof {
[INFO] [stdout]     |     ----- while parsing this struct
[INFO] [stdout] 341 |         gauth.update(&mut gvar, 2);
[INFO] [stdout]     |         -----^ expected one of `,`, `:`, or `}`
[INFO] [stdout]     |         |
[INFO] [stdout]     |         while parsing this struct field
[INFO] [stdout]     |
[INFO] [stdout] help: try naming a field
[INFO] [stdout]     |
[INFO] [stdout] 341 |         gauth: gauth.update(&mut gvar, 2);
[INFO] [stdout]     |         ++++++
[INFO] [stdout] 
[INFO] [stdout] error: expected identifier, found `2`
[INFO] [stdout]    --> tokens/frac.rs:341:33
[INFO] [stdout]     |
[INFO] [stdout] 340 |     proof {
[INFO] [stdout]     |     ----- while parsing this struct
[INFO] [stdout] 341 |         gauth.update(&mut gvar, 2);
[INFO] [stdout]     |                                 ^ expected identifier
[INFO] [stdout] 
[INFO] [stdout] error: expected `;`, found `assert`
[INFO] [stdout]    --> tokens/frac.rs:342:6
[INFO] [stdout]     |
[INFO] [stdout] 342 |     }
[INFO] [stdout]     |      ^ help: add `;` here
[INFO] [stdout] 343 |     assert(gauth@ == 2);
[INFO] [stdout]     |     ------ unexpected token
[INFO] [stdout] 
[INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `@`
[INFO] [stdout]    --> tokens/frac.rs:343:17
[INFO] [stdout]     |
[INFO] [stdout] 343 |     assert(gauth@ == 2);
[INFO] [stdout]     |                 ^ expected one of 8 possible tokens
[INFO] [stdout] 
[INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `@`
[INFO] [stdout]    --> tokens/frac.rs:344:16
[INFO] [stdout]     |
[INFO] [stdout] 344 |     assert(gvar@ == 2);
[INFO] [stdout]     |                ^ expected one of 8 possible tokens
[INFO] [stdout] 
[INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `tracked` in this scope
[INFO] [stdout]    --> tokens/frac.rs:337:9
[INFO] [stdout]     |
[INFO] [stdout] 337 |     let tracked (mut gauth, mut gvar) = GhostVarAuth::<u64>::new(1);
[INFO] [stdout]     |         ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `GhostVarAuth` in this scope
[INFO] [stdout]    --> tokens/frac.rs:337:41
[INFO] [stdout]     |
[INFO] [stdout] 337 |     let tracked (mut gauth, mut gvar) = GhostVarAuth::<u64>::new(1);
[INFO] [stdout]     |                                         ^^^^^^^^^^^^ use of undeclared type `GhostVarAuth`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 9 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0433, E0531.
[INFO] [stdout] For more information about an error, try `rustc --explain E0433`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] 
[INFO] [stdout] failures:
[INFO] [stdout]     arithmetic/overflow.rs - arithmetic::overflow (line 13)
[INFO] [stdout]     atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 230)
[INFO] [stdout]     atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 299)
[INFO] [stdout]     calc_macro.rs - calc_macro::calc (line 17)
[INFO] [stdout]     calc_macro.rs - calc_macro::calc (line 37)
[INFO] [stdout]     invariant.rs - invariant::open_atomic_invariant (line 355)
[INFO] [stdout]     invariant.rs - invariant::open_local_invariant (line 462)
[INFO] [stdout]     invariant.rs - invariant::open_local_invariant (line 483)
[INFO] [stdout]     invariant.rs - invariant::open_local_invariant (line 499)
[INFO] [stdout]     invariant.rs - invariant::open_local_invariant (line 508)
[INFO] [stdout]     map.rs - map::assert_maps_equal (line 355)
[INFO] [stdout]     map.rs - map::assert_maps_equal (line 368)
[INFO] [stdout]     pervasive.rs - pervasive::assert_by_contradiction (line 225)
[INFO] [stdout]     pervasive.rs - pervasive::struct_with_invariants (line 276)
[INFO] [stdout]     pervasive.rs - pervasive::struct_with_invariants (line 306)
[INFO] [stdout]     seq.rs - seq::seq (line 541)
[INFO] [stdout]     seq_lib.rs - seq_lib::assert_seqs_equal (line 3557)
[INFO] [stdout]     seq_lib.rs - seq_lib::assert_seqs_equal (line 3576)
[INFO] [stdout]     set_lib.rs - set_lib::assert_sets_equal (line 1505)
[INFO] [stdout]     set_lib.rs - set_lib::assert_sets_equal (line 1511)
[INFO] [stdout]     simple_pptr.rs - simple_pptr::PPtr (line 118)
[INFO] [stdout]     simple_pptr.rs - simple_pptr::PPtr (line 58)
[INFO] [stdout]     simple_pptr.rs - simple_pptr::PPtr (line 92)
[INFO] [stdout]     tokens/frac.rs - tokens::frac::FracGhost (line 86)
[INFO] [stdout]     tokens/frac.rs - tokens::frac::GhostVarAuth (line 335)
[INFO] [stdout]     tokens/map.rs - tokens::map (line 19)
[INFO] [stdout]     tokens/seq.rs - tokens::seq::GhostSeqAuth (line 23)
[INFO] [stdout]     tokens/set.rs - tokens::set (line 20)
[INFO] [stdout] 
[INFO] [stdout] test result: FAILED. 1 passed; 28 failed; 7 ignored; 0 measured; 0 filtered out; finished in 1.28s
[INFO] [stdout] 
[INFO] [stderr] error: doctest failed, to rerun pass `--doc`
[INFO] running `Command { std: "docker" "inspect" "656c39cefc06b917a49322ef4f2ef0d3279222d90305047af30ea97622cb70da", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "rm" "-f" "656c39cefc06b917a49322ef4f2ef0d3279222d90305047af30ea97622cb70da", kill_on_drop: false }`
[INFO] [stdout] 656c39cefc06b917a49322ef4f2ef0d3279222d90305047af30ea97622cb70da
