[INFO] fetching crate verus_builtin_macros 0.0.0-2026-09-20-0158...
[INFO] testing verus_builtin_macros-0.0.0-2026-09-20-0158 against 1.100.0-beta.1 for beta-1.100-2
[INFO] extracting crate verus_builtin_macros 0.0.0-2026-09-20-0158 into /workspace/builds/worker-3-tc2/source
[INFO] started tweaking crates.io crate verus_builtin_macros 0.0.0-2026-09-20-0158
[INFO] finished tweaking crates.io crate verus_builtin_macros 0.0.0-2026-09-20-0158
[INFO] tweaked toml for crates.io crate verus_builtin_macros 0.0.0-2026-09-20-0158 written to /workspace/builds/worker-3-tc2/source/Cargo.toml
[INFO] validating manifest of crates.io crate verus_builtin_macros 0.0.0-2026-09-20-0158 on toolchain 1.100.0-beta.1
[INFO] running `Command { std: CARGO_HOME="/workspace/cargo-home" RUSTUP_HOME="/workspace/rustup-home" "/workspace/cargo-home/bin/cargo" "+1.100.0-beta.1" "metadata" "--manifest-path" "Cargo.toml" "--no-deps", kill_on_drop: false }`
[INFO] crate crates.io crate verus_builtin_macros 0.0.0-2026-09-20-0158 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.100.0-beta.1" "fetch" "--manifest-path" "Cargo.toml", kill_on_drop: false }`
[INFO] [stderr] warning: `package.homepage` is redundant with `package.repository`
[INFO] [stderr]    --> Cargo.toml:139:12
[INFO] [stderr]     |
[INFO] [stderr] 139 | homepage = "https://github.com/verus-lang/verus"
[INFO] [stderr]     |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[INFO] [stderr] ...
[INFO] [stderr] 144 | repository = "https://github.com/verus-lang/verus"
[INFO] [stderr]     |              -------------------------------------
[INFO] [stderr]     |
[INFO] [stderr]     = note: `cargo::redundant_homepage` is set to `warn` by default
[INFO] [stderr] help: consider removing `package.homepage`
[INFO] [stderr] warning: `verus_builtin_macros` (manifest) generated 1 warning
[INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-3-tc2/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-3-tc2/target:/opt/rustwide/target:rw,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" "-m" "1610612736" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:3111399a4047eeb3a02b7a90e478d715f38a8c6669b5c4b49d30a17385265909" "sleep" "infinity", kill_on_drop: false }`
[INFO] [stdout] 709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95
[INFO] running `Command { std: "docker" "start" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "inspect" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "exec" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-w" "/opt/rustwide/workdir" "--user" "0:0" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95" "/opt/rustwide/cargo-home/bin/cargo" "+1.100.0-beta.1" "metadata" "--no-deps" "--format-version=1", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "inspect" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "exec" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-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" "-w" "/opt/rustwide/workdir" "--user" "0:0" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95" "/opt/rustwide/cargo-home/bin/cargo" "+1.100.0-beta.1" "build" "--frozen" "--message-format=json", kill_on_drop: false }`
[INFO] [stderr] warning: `package.homepage` is redundant with `package.repository`
[INFO] [stderr]    --> Cargo.toml:139:12
[INFO] [stderr]     |
[INFO] [stderr] 139 | homepage = "https://github.com/verus-lang/verus"
[INFO] [stderr]     |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[INFO] [stderr] ...
[INFO] [stderr] 144 | repository = "https://github.com/verus-lang/verus"
[INFO] [stderr]     |              -------------------------------------
[INFO] [stderr]     |
[INFO] [stderr]     = note: `cargo::redundant_homepage` is set to `warn` by default
[INFO] [stderr] help: consider removing `package.homepage`
[INFO] [stderr] warning: `verus_builtin_macros` (manifest) generated 1 warning
[INFO] [stderr]    Compiling proc-macro2 v1.0.107
[INFO] [stderr]    Compiling verus_prettyplease v0.0.0-2026-09-06-0133
[INFO] [stderr]    Compiling convert_case v0.4.0
[INFO] [stderr]    Compiling quote v1.0.47
[INFO] [stderr]    Compiling verus_syn v0.0.0-2026-09-06-0133
[INFO] [stderr]    Compiling syn v2.0.119
[INFO] [stderr]    Compiling synstructure v0.13.2
[INFO] [stderr]    Compiling verus_builtin_macros v0.0.0-2026-09-20-0158 (/opt/rustwide/workdir)
[INFO] [stderr]     Finished `dev` profile [unoptimized + debuginfo] target(s) in 14.95s
[INFO] running `Command { std: "docker" "inspect" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "exec" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-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" "-w" "/opt/rustwide/workdir" "--user" "0:0" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95" "/opt/rustwide/cargo-home/bin/cargo" "+1.100.0-beta.1" "test" "--frozen" "--no-run" "--message-format=json", kill_on_drop: false }`
[INFO] [stderr] warning: `package.homepage` is redundant with `package.repository`
[INFO] [stderr]    --> Cargo.toml:139:12
[INFO] [stderr]     |
[INFO] [stderr] 139 | homepage = "https://github.com/verus-lang/verus"
[INFO] [stderr]     |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[INFO] [stderr] ...
[INFO] [stderr] 144 | repository = "https://github.com/verus-lang/verus"
[INFO] [stderr]     |              -------------------------------------
[INFO] [stderr]     |
[INFO] [stderr]     = note: `cargo::redundant_homepage` is set to `warn` by default
[INFO] [stderr] help: consider removing `package.homepage`
[INFO] [stderr] warning: `verus_builtin_macros` (manifest) generated 1 warning
[INFO] [stderr]    Compiling verus_builtin_macros v0.0.0-2026-09-20-0158 (/opt/rustwide/workdir)
[INFO] [stderr]     Finished `test` profile [unoptimized + debuginfo] target(s) in 5.91s
[INFO] running `Command { std: "docker" "inspect" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "exec" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-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" "-w" "/opt/rustwide/workdir" "--user" "0:0" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95" "/opt/rustwide/cargo-home/bin/cargo" "+1.100.0-beta.1" "test" "--frozen", kill_on_drop: false }`
[INFO] [stderr] warning: `package.homepage` is redundant with `package.repository`
[INFO] [stderr]    --> Cargo.toml:139:12
[INFO] [stderr]     |
[INFO] [stderr] 139 | homepage = "https://github.com/verus-lang/verus"
[INFO] [stderr]     |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[INFO] [stderr] ...
[INFO] [stderr] 144 | repository = "https://github.com/verus-lang/verus"
[INFO] [stderr]     |              -------------------------------------
[INFO] [stderr]     |
[INFO] [stderr]     = note: `cargo::redundant_homepage` is set to `warn` by default
[INFO] [stderr] help: consider removing `package.homepage`
[INFO] [stderr] warning: `verus_builtin_macros` (manifest) generated 1 warning
[INFO] [stderr]     Finished `test` profile [unoptimized + debuginfo] target(s) in 0.03s
[INFO] [stderr]      Running unittests src/lib.rs (/opt/rustwide/target/debug/build/verus_builtin_macros/75c109518f0d3e14/out/verus_builtin_macros-75c109518f0d3e14)
[INFO] [stderr]    Doc-tests verus_builtin_macros
[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] [stdout] 
[INFO] [stdout] running 28 tests
[INFO] [stdout] test src/contrib/exec_spec.rs - contrib::exec_spec::replace_self_tokens (line 742) ... ignored
[INFO] [stdout] test src/contrib/hooks.rs - contrib::hooks (line 27) ... ignored
[INFO] [stdout] test src/contrib/hooks.rs - contrib::hooks (line 42) ... ignored
[INFO] [stdout] test src/contrib/hooks.rs - contrib::hooks (line 53) ... ignored
[INFO] [stdout] test src/lib.rs - exec_spec_verified (line 594) ... ignored
[INFO] [stdout] test src/lib.rs - set_build (line 441) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 498) ... FAILED
[INFO] [stdout] test src/contrib/spec_derive.rs - contrib::spec_derive::make_spec_type (line 26) ... FAILED
[INFO] [stdout] test src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 949) ... FAILED
[INFO] [stdout] test src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 927) ... FAILED
[INFO] [stdout] test src/contrib/spec_derive.rs - contrib::spec_derive::self_view (line 580) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 492) ... FAILED
[INFO] [stdout] test src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 933) ... FAILED
[INFO] [stdout] test src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 944) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 485) ... FAILED
[INFO] [stdout] test src/unerased_proxies.rs - unerased_proxies (line 43) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 478) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 472) ... FAILED
[INFO] [stdout] test src/unerased_proxies.rs - unerased_proxies (line 52) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 467) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 534) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 453) ... FAILED
[INFO] [stdout] test src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 919) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 460) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 544) ... FAILED
[INFO] [stdout] test src/lib.rs - set_build (line 518) ... FAILED
[INFO] [stdout] test src/unerased_proxies.rs - unerased_proxies (line 17) ... FAILED
[INFO] [stdout] test src/unerased_proxies.rs - unerased_proxies (line 26) ... FAILED
[INFO] [stdout] 
[INFO] [stdout] failures:
[INFO] [stdout] 
[INFO] [stdout] ---- src/lib.rs - set_build (line 441) stdout ----
[INFO] [stdout] error: expected one of `!` or `::`, found keyword `fn`
[INFO] [stdout]    --> src/lib.rs:442:7
[INFO] [stdout]     |
[INFO] [stdout] 442 | proof fn test() {
[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] ---- src/lib.rs - set_build (line 498) stdout ----
[INFO] [stdout] error: expected one of `!` or `::`, found keyword `fn`
[INFO] [stdout]    --> src/lib.rs:504:7
[INFO] [stdout]     |
[INFO] [stdout] 504 | proof fn test() {
[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] ---- src/contrib/spec_derive.rs - contrib::spec_derive::make_spec_type (line 26) stdout ----
[INFO] [stdout] error: cannot find attribute `make_spec_type` in this scope
[INFO] [stdout]   --> src/contrib/spec_derive.rs:27:3
[INFO] [stdout]    |
[INFO] [stdout] 27 | #[make_spec_type(exclude(private_field))]
[INFO] [stdout]    |   ^^^^^^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0392]: lifetime parameter `'a` is never used
[INFO] [stdout]   --> src/contrib/spec_derive.rs:28:21
[INFO] [stdout]    |
[INFO] [stdout] 28 | pub struct MyStruct<'a> {
[INFO] [stdout]    |                     ^^ unused lifetime parameter
[INFO] [stdout]    |
[INFO] [stdout]    = help: consider removing `'a`, referring to it in a field, or using a marker such as `PhantomData`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 2 previous errors
[INFO] [stdout] 
[INFO] [stdout] For more information about this error, try `rustc --explain E0392`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 949) stdout ----
[INFO] [stdout] error: expected item, found keyword `let`
[INFO] [stdout]    --> src/attr_rewrite.rs:950:1
[INFO] [stdout]     |
[INFO] [stdout] 950 | let tracked mut out;
[INFO] [stdout]     | ^^^
[INFO] [stdout]     | |
[INFO] [stdout]     | `let` cannot be used for global variables
[INFO] [stdout]     | help: consider using `static` or `const` instead of `let`
[INFO] [stdout]     |
[INFO] [stdout]     = note: for a full list of items that can appear in modules, see <https://doc.rust-lang.org/reference/items.html>
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 927) stdout ----
[INFO] [stdout] error[E0658]: attributes on expressions are experimental
[INFO] [stdout]    --> src/attr_rewrite.rs:928:4
[INFO] [stdout]     |
[INFO] [stdout] 928 | if #[verus_io(with Tracked(arg1), Ghost(arg2) -> Tracked(out) |= Tracked(extra))]
[INFO] [stdout]     |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[INFO] [stdout]     |
[INFO] [stdout]     = note: see issue #15701 <https://github.com/rust-lang/rust/issues/15701> for more information
[INFO] [stdout] 
[INFO] [stdout] error: cannot find attribute `verus_io` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:928:6
[INFO] [stdout]     |
[INFO] [stdout] 928 | if #[verus_io(with Tracked(arg1), Ghost(arg2) -> Tracked(out) |= Tracked(extra))]
[INFO] [stdout]     |      ^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find value `arg0` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:929:6
[INFO] [stdout]     |
[INFO] [stdout] 929 | call(arg0) == something {
[INFO] [stdout]     |      ^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find value `something` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:929:15
[INFO] [stdout]     |
[INFO] [stdout] 929 | call(arg0) == something {
[INFO] [stdout]     |               ^^^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function `call` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:929:1
[INFO] [stdout]     |
[INFO] [stdout] 929 | call(arg0) == something {
[INFO] [stdout]     | ^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 5 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0425, E0658.
[INFO] [stdout] For more information about an error, try `rustc --explain E0425`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/contrib/spec_derive.rs - contrib::spec_derive::self_view (line 580) stdout ----
[INFO] [stdout] error: cannot find attribute `self_view` in this scope
[INFO] [stdout]    --> src/contrib/spec_derive.rs:581:3
[INFO] [stdout]     |
[INFO] [stdout] 581 | #[self_view]
[INFO] [stdout]     |   ^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/lib.rs - set_build (line 492) stdout ----
[INFO] [stdout] error: `~` cannot be used as a unary operator
[INFO] [stdout]    --> src/lib.rs:493:12
[INFO] [stdout]     |
[INFO] [stdout] 493 | assert(s1 =~= s2);
[INFO] [stdout]     |            ^
[INFO] [stdout]     |
[INFO] [stdout] help: use `!` to perform bitwise not
[INFO] [stdout]     |
[INFO] [stdout] 493 - assert(s1 =~= s2);
[INFO] [stdout] 493 + assert(s1 =!= s2);
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error: expected `:`, found `=`
[INFO] [stdout]    --> src/lib.rs:493:11
[INFO] [stdout]     |
[INFO] [stdout] 493 | assert(s1 =~= s2);
[INFO] [stdout]     |           ^
[INFO] [stdout]     |
[INFO] [stdout] help: replace equals symbol with a colon
[INFO] [stdout]     |
[INFO] [stdout] 493 - assert(s1 =~= s2);
[INFO] [stdout] 493 + assert(s1:~= s2);
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error: expected expression, found `=`
[INFO] [stdout]    --> src/lib.rs:493:13
[INFO] [stdout]     |
[INFO] [stdout] 493 | assert(s1 =~= s2);
[INFO] [stdout]     |             ^ expected expression
[INFO] [stdout] 
[INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `:`
[INFO] [stdout]    --> src/lib.rs:494:16
[INFO] [stdout]     |
[INFO] [stdout] 494 | assert(forall|p: (u8, u8)| s1.contains(p) <==> p.0 == p.1 && p.0 < 100);
[INFO] [stdout]     |                ^ expected one of 8 possible tokens
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 4 previous errors
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 933) stdout ----
[INFO] [stdout] error: cannot find macro `proof` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:936:5
[INFO] [stdout]     |
[INFO] [stdout] 936 |     proof!{out = tmp_out.get();}  // Ensuring `out` is properly assigned.
[INFO] [stdout]     |     ^^^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find value `arg0` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:935:31
[INFO] [stdout]     |
[INFO] [stdout] 935 |     let (tmp, tmp_out) = call(arg0, Tracked(arg1), Tracked(arg2));
[INFO] [stdout]     |                               ^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find value `arg1` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:935:45
[INFO] [stdout]     |
[INFO] [stdout] 935 |     let (tmp, tmp_out) = call(arg0, Tracked(arg1), Tracked(arg2));
[INFO] [stdout]     |                                             ^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find value `arg2` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:935:60
[INFO] [stdout]     |
[INFO] [stdout] 935 |     let (tmp, tmp_out) = call(arg0, Tracked(arg1), Tracked(arg2));
[INFO] [stdout]     |                                                            ^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find value `extra` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:937:19
[INFO] [stdout]     |
[INFO] [stdout] 937 |     (tmp, Tracked(extra))  // Returning the transformed values.
[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]    --> src/attr_rewrite.rs:935:37
[INFO] [stdout]     |
[INFO] [stdout] 935 |     let (tmp, tmp_out) = call(arg0, Tracked(arg1), Tracked(arg2));
[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]    --> src/attr_rewrite.rs:935:52
[INFO] [stdout]     |
[INFO] [stdout] 935 |     let (tmp, tmp_out) = call(arg0, Tracked(arg1), Tracked(arg2));
[INFO] [stdout]     |                                                    ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function `call` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:935:26
[INFO] [stdout]     |
[INFO] [stdout] 935 |     let (tmp, tmp_out) = call(arg0, Tracked(arg1), Tracked(arg2));
[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]    --> src/attr_rewrite.rs:937:11
[INFO] [stdout]     |
[INFO] [stdout] 937 |     (tmp, Tracked(extra))  // Returning the transformed values.
[INFO] [stdout]     |           ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 9 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] ---- src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 944) stdout ----
[INFO] [stdout] error: cannot find attribute `verus_spec` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:945:3
[INFO] [stdout]     |
[INFO] [stdout] 945 | #[verus_spec(with Tracked(arg1), Ghost(arg2) -> Tracked(out) |= Tracked(extra))]
[INFO] [stdout]     |   ^^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find value `arg0` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:946:17
[INFO] [stdout]     |
[INFO] [stdout] 946 | let out0 = call(arg0);
[INFO] [stdout]     |                 ^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find function `call` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:946:12
[INFO] [stdout]     |
[INFO] [stdout] 946 | let out0 = call(arg0);
[INFO] [stdout]     |            ^^^^ not found in this scope
[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] ---- src/lib.rs - set_build (line 485) stdout ----
[INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `:`
[INFO] [stdout]    --> src/lib.rs:486:16
[INFO] [stdout]     |
[INFO] [stdout] 486 | assert(forall|p: (u8, u8)| s1.contains(p) <==> p.0 == p.1 && p.0 < 100); // FAILS
[INFO] [stdout]     |                ^ expected one of 8 possible tokens
[INFO] [stdout] 
[INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `:`
[INFO] [stdout]    --> src/lib.rs:487:16
[INFO] [stdout]     |
[INFO] [stdout] 487 | assert(forall|p: (u8, u8)| s2.contains(p) <==> p.0 == p.1 && p.0 < 100);
[INFO] [stdout]     |                ^ expected one of 8 possible tokens
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 2 previous errors
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/unerased_proxies.rs - unerased_proxies (line 43) stdout ----
[INFO] [stdout] error: return types are denoted using `->`
[INFO] [stdout]   --> src/unerased_proxies.rs:44:19
[INFO] [stdout]    |
[INFO] [stdout] 44 | const fn x(t: u64): u64 = {
[INFO] [stdout]    |                   ^
[INFO] [stdout]    |
[INFO] [stdout] help: use `->` instead
[INFO] [stdout]    |
[INFO] [stdout] 44 - const fn x(t: u64): u64 = {
[INFO] [stdout] 44 + const fn x(t: u64) -> u64 = {
[INFO] [stdout]    |
[INFO] [stdout] 
[INFO] [stdout] error: expected `;`, found `}`
[INFO] [stdout]   --> src/unerased_proxies.rs:47:2
[INFO] [stdout]    |
[INFO] [stdout] 47 | }
[INFO] [stdout]    |  ^ help: add `;` here
[INFO] [stdout] 48 | } _doctest_main_src_unerased_proxies_rs_43_0() }
[INFO] [stdout]    | - unexpected token
[INFO] [stdout] 
[INFO] [stdout] error: function body cannot be `= expression;`
[INFO] [stdout]   --> src/unerased_proxies.rs:44:25
[INFO] [stdout]    |
[INFO] [stdout] 44 |   const fn x(t: u64): u64 = {
[INFO] [stdout]    |  _________________________^
[INFO] [stdout] 45 | |     assert(true);
[INFO] [stdout] 46 | |     x
[INFO] [stdout] 47 | | }
[INFO] [stdout]    | |_^
[INFO] [stdout]    |
[INFO] [stdout] help: surround the expression with `{` and `}` instead of `=` and `;`
[INFO] [stdout]    |
[INFO] [stdout] 44 ~ const fn x(t: u64): u64 { {
[INFO] [stdout] 45 |     assert(true);
[INFO] [stdout] 46 |     x
[INFO] [stdout] 47 ~  }
[INFO] [stdout]    |
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 3 previous errors
[INFO] [stdout] 
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/lib.rs - set_build (line 478) stdout ----
[INFO] [stdout] error[E0433]: cannot find type `Set` in this scope
[INFO] [stdout]    --> src/lib.rs:479:1
[INFO] [stdout]     |
[INFO] [stdout] 479 | Set::<u8>::from_finite_type(|x: u8| true)
[INFO] [stdout]     | ^^^ use of undeclared type `Set`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] For more information about this error, try `rustc --explain E0433`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/lib.rs - set_build (line 472) stdout ----
[INFO] [stdout] error[E0433]: cannot find type `Set` in this scope
[INFO] [stdout]    --> src/lib.rs:473:1
[INFO] [stdout]     |
[INFO] [stdout] 473 | Set::<u8>::from_finite_type(|x: u8| true)
[INFO] [stdout]     | ^^^ use of undeclared type `Set`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] For more information about this error, try `rustc --explain E0433`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/unerased_proxies.rs - unerased_proxies (line 52) stdout ----
[INFO] [stdout] error: return types are denoted using `->`
[INFO] [stdout]   --> src/unerased_proxies.rs:54:35
[INFO] [stdout]    |
[INFO] [stdout] 54 | fn VERUS_UNERASED_PROXY__x(t: u64): u64 = {
[INFO] [stdout]    |                                   ^
[INFO] [stdout]    |
[INFO] [stdout] help: use `->` instead
[INFO] [stdout]    |
[INFO] [stdout] 54 - fn VERUS_UNERASED_PROXY__x(t: u64): u64 = {
[INFO] [stdout] 54 + fn VERUS_UNERASED_PROXY__x(t: u64) -> u64 = {
[INFO] [stdout]    |
[INFO] [stdout] 
[INFO] [stdout] error: expected `;`, found `#`
[INFO] [stdout]   --> src/unerased_proxies.rs:57:2
[INFO] [stdout]    |
[INFO] [stdout] 57 | }
[INFO] [stdout]    |  ^ help: add `;` here
[INFO] [stdout] 58 |
[INFO] [stdout] 59 | #[verifier::external]
[INFO] [stdout]    | - unexpected token
[INFO] [stdout] 
[INFO] [stdout] error: function body cannot be `= expression;`
[INFO] [stdout]   --> src/unerased_proxies.rs:54:41
[INFO] [stdout]    |
[INFO] [stdout] 54 |   fn VERUS_UNERASED_PROXY__x(t: u64): u64 = {
[INFO] [stdout]    |  _________________________________________^
[INFO] [stdout] 55 | |     assert(true);
[INFO] [stdout] 56 | |     x
[INFO] [stdout] 57 | | }
[INFO] [stdout]    | |_^
[INFO] [stdout]    |
[INFO] [stdout] help: surround the expression with `{` and `}` instead of `=` and `;`
[INFO] [stdout]    |
[INFO] [stdout] 54 ~ fn VERUS_UNERASED_PROXY__x(t: u64): u64 { {
[INFO] [stdout] 55 |     assert(true);
[INFO] [stdout] 56 |     x
[INFO] [stdout] 57 ~  }
[INFO] [stdout]    |
[INFO] [stdout] 
[INFO] [stdout] error: return types are denoted using `->`
[INFO] [stdout]   --> src/unerased_proxies.rs:61:19
[INFO] [stdout]    |
[INFO] [stdout] 61 | const fn x(t: u64): u64 = {
[INFO] [stdout]    |                   ^
[INFO] [stdout]    |
[INFO] [stdout] help: use `->` instead
[INFO] [stdout]    |
[INFO] [stdout] 61 - const fn x(t: u64): u64 = {
[INFO] [stdout] 61 + const fn x(t: u64) -> u64 = {
[INFO] [stdout]    |
[INFO] [stdout] 
[INFO] [stdout] error: expected `;`, found `}`
[INFO] [stdout]   --> src/unerased_proxies.rs:63:2
[INFO] [stdout]    |
[INFO] [stdout] 63 | }
[INFO] [stdout]    |  ^ help: add `;` here
[INFO] [stdout] 64 | } _doctest_main_src_unerased_proxies_rs_52_0() }
[INFO] [stdout]    | - unexpected token
[INFO] [stdout] 
[INFO] [stdout] error: function body cannot be `= expression;`
[INFO] [stdout]   --> src/unerased_proxies.rs:61:25
[INFO] [stdout]    |
[INFO] [stdout] 61 |   const fn x(t: u64): u64 = {
[INFO] [stdout]    |  _________________________^
[INFO] [stdout] 62 | |     x
[INFO] [stdout] 63 | | }
[INFO] [stdout]    | |_^
[INFO] [stdout]    |
[INFO] [stdout] help: surround the expression with `{` and `}` instead of `=` and `;`
[INFO] [stdout]    |
[INFO] [stdout] 61 ~ const fn x(t: u64): u64 { {
[INFO] [stdout] 62 |     x
[INFO] [stdout] 63 ~  }
[INFO] [stdout]    |
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find module or crate `verifier` in this scope
[INFO] [stdout]   --> src/unerased_proxies.rs:59:3
[INFO] [stdout]    |
[INFO] [stdout] 59 | #[verifier::external]
[INFO] [stdout]    |   ^^^^^^^^ use of unresolved module or unlinked crate `verifier`
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find module or crate `verus` in this scope
[INFO] [stdout]   --> src/unerased_proxies.rs:60:3
[INFO] [stdout]    |
[INFO] [stdout] 60 | #[verus::internal(has_unerased_proxy)]
[INFO] [stdout]    |   ^^^^^ use of unresolved module or unlinked crate `verus`
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find module or crate `verus` in this scope
[INFO] [stdout]   --> src/unerased_proxies.rs:53:3
[INFO] [stdout]    |
[INFO] [stdout] 53 | #[verus::internal(unerased_proxy)]
[INFO] [stdout]    |   ^^^^^ use of unresolved module or unlinked crate `verus`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 9 previous errors
[INFO] [stdout] 
[INFO] [stdout] For more information about this error, try `rustc --explain E0433`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/lib.rs - set_build (line 467) stdout ----
[INFO] [stdout] error: cannot find macro `set_build` in this scope
[INFO] [stdout]    --> src/lib.rs:468:25
[INFO] [stdout]     |
[INFO] [stdout] 468 | let s1: Set<(u8, u8)> = set_build!{ (x, x): (u8, u8) | exists x: u8, x < 100 };
[INFO] [stdout]     |                         ^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error: cannot find macro `set_build` in this scope
[INFO] [stdout]    --> src/lib.rs:469:25
[INFO] [stdout]     |
[INFO] [stdout] 469 | let s2: Set<(u8, u8)> = set_build!{ (x, x): (u8, u8) | x: u8, x < 100 };
[INFO] [stdout]     |                         ^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `Set` in this scope
[INFO] [stdout]    --> src/lib.rs:468:9
[INFO] [stdout]     |
[INFO] [stdout] 468 | let s1: Set<(u8, u8)> = set_build!{ (x, x): (u8, u8) | exists x: u8, x < 100 };
[INFO] [stdout]     |         ^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `Set` in this scope
[INFO] [stdout]    --> src/lib.rs:469:9
[INFO] [stdout]     |
[INFO] [stdout] 469 | let s2: Set<(u8, u8)> = set_build!{ (x, x): (u8, u8) | x: u8, x < 100 };
[INFO] [stdout]     |         ^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 4 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] ---- src/lib.rs - set_build (line 534) stdout ----
[INFO] [stdout] error: cannot find macro `set_build` in this scope
[INFO] [stdout]    --> src/lib.rs:535:9
[INFO] [stdout]     |
[INFO] [stdout] 535 | let s = set_build!{ (x, y, y - x): (int, int, int) | x: int in 10..20, y: int in x..20, x + y != 25 };
[INFO] [stdout]     |         ^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: cannot find function `assert` in this scope
[INFO] [stdout]    --> src/lib.rs:536:1
[INFO] [stdout]     |
[INFO] [stdout] 536 | assert(s.contains((12, 14, 2)));
[INFO] [stdout]     | ^^^^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout]     = note: a macro named `assert` exists in another namespace
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]     |
[INFO] [stdout] 536 | assert!(s.contains((12, 14, 2)));
[INFO] [stdout]     |       +
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: cannot find function `assert` in this scope
[INFO] [stdout]    --> src/lib.rs:537:1
[INFO] [stdout]     |
[INFO] [stdout] 537 | assert(!s.contains((14, 12, 2))); // because y = 12 is not in 14..20
[INFO] [stdout]     | ^^^^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout]     = note: a macro named `assert` exists in another namespace
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]     |
[INFO] [stdout] 537 | assert!(!s.contains((14, 12, 2))); // because y = 12 is not in 14..20
[INFO] [stdout]     |       +
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: cannot find function `assert` in this scope
[INFO] [stdout]    --> src/lib.rs:538:1
[INFO] [stdout]     |
[INFO] [stdout] 538 | assert(s.contains((10, 13, 3)));
[INFO] [stdout]     | ^^^^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout]     = note: a macro named `assert` exists in another namespace
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]     |
[INFO] [stdout] 538 | assert!(s.contains((10, 13, 3)));
[INFO] [stdout]     |       +
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: cannot find function `assert` in this scope
[INFO] [stdout]    --> src/lib.rs:539:1
[INFO] [stdout]     |
[INFO] [stdout] 539 | assert(s.contains((10, 14, 4)));
[INFO] [stdout]     | ^^^^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout]     = note: a macro named `assert` exists in another namespace
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]     |
[INFO] [stdout] 539 | assert!(s.contains((10, 14, 4)));
[INFO] [stdout]     |       +
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: cannot find function `assert` in this scope
[INFO] [stdout]    --> src/lib.rs:540:1
[INFO] [stdout]     |
[INFO] [stdout] 540 | assert(!s.contains((10, 15, 5))); // because of x + y != 25
[INFO] [stdout]     | ^^^^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout]     = note: a macro named `assert` exists in another namespace
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]     |
[INFO] [stdout] 540 | assert!(!s.contains((10, 15, 5))); // because of x + y != 25
[INFO] [stdout]     |       +
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: cannot find function `assert` in this scope
[INFO] [stdout]    --> src/lib.rs:541:1
[INFO] [stdout]     |
[INFO] [stdout] 541 | assert(s.contains((10, 16, 6)));
[INFO] [stdout]     | ^^^^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout]     = note: a macro named `assert` exists in another namespace
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]     |
[INFO] [stdout] 541 | assert!(s.contains((10, 16, 6)));
[INFO] [stdout]     |       +
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 7 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] ---- src/lib.rs - set_build (line 453) stdout ----
[INFO] [stdout] error: expected identifier, found `:`
[INFO] [stdout]    --> src/lib.rs:455:16
[INFO] [stdout]     |
[INFO] [stdout] 455 | assert(forall|u: u8| s.contains(u) <==> u < 100);
[INFO] [stdout]     |                ^ expected identifier
[INFO] [stdout] 
[INFO] [stdout] error: cannot find macro `set_build` in this scope
[INFO] [stdout]    --> src/lib.rs:454:18
[INFO] [stdout]     |
[INFO] [stdout] 454 | let s: Set<u8> = set_build!{ x: u8, x < 100 };
[INFO] [stdout]     |                  ^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `Set` in this scope
[INFO] [stdout]    --> src/lib.rs:454:8
[INFO] [stdout]     |
[INFO] [stdout] 454 | let s: Set<u8> = set_build!{ x: u8, x < 100 };
[INFO] [stdout]     |        ^^^ not found in this scope
[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] ---- src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 919) stdout ----
[INFO] [stdout] error[E0658]: attributes on expressions are experimental
[INFO] [stdout]    --> src/attr_rewrite.rs:920:2
[INFO] [stdout]     |
[INFO] [stdout] 920 | {#[verus_spec(with ..)] expr};
[INFO] [stdout]     |  ^^^^^^^^^^^^^^^^^^^^^^
[INFO] [stdout]     |
[INFO] [stdout]     = note: see issue #15701 <https://github.com/rust-lang/rust/issues/15701> for more information
[INFO] [stdout] 
[INFO] [stdout] error: cannot find attribute `verus_spec` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:920:4
[INFO] [stdout]     |
[INFO] [stdout] 920 | {#[verus_spec(with ..)] expr};
[INFO] [stdout]     |    ^^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find value `expr` in this scope
[INFO] [stdout]    --> src/attr_rewrite.rs:920:25
[INFO] [stdout]     |
[INFO] [stdout] 920 | {#[verus_spec(with ..)] expr};
[INFO] [stdout]     |                         ^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 3 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0425, E0658.
[INFO] [stdout] For more information about an error, try `rustc --explain E0425`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/lib.rs - set_build (line 460) stdout ----
[INFO] [stdout] error: expected identifier, found `:`
[INFO] [stdout]    --> src/lib.rs:462:16
[INFO] [stdout]     |
[INFO] [stdout] 462 | assert(forall|u: u8| s.contains(u) <==> 10 <= u < 20);
[INFO] [stdout]     |                ^ expected identifier
[INFO] [stdout] 
[INFO] [stdout] error: cannot find macro `set_build` in this scope
[INFO] [stdout]    --> src/lib.rs:461:18
[INFO] [stdout]     |
[INFO] [stdout] 461 | let s: Set<u8> = set_build!{ x: u8 in 10..20 };
[INFO] [stdout]     |                  ^^^^^^^^^
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `Set` in this scope
[INFO] [stdout]    --> src/lib.rs:461:8
[INFO] [stdout]     |
[INFO] [stdout] 461 | let s: Set<u8> = set_build!{ x: u8 in 10..20 };
[INFO] [stdout]     |        ^^^ not found in this scope
[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] ---- src/lib.rs - set_build (line 544) stdout ----
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:545:7
[INFO] [stdout]     |
[INFO] [stdout] 545 | Set::<int>::range(10, 20)
[INFO] [stdout]     |       ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 545 - Set::<int>::range(10, 20)
[INFO] [stdout] 545 + Set::<i32>::range(10, 20)
[INFO] [stdout]     |
[INFO] [stdout] help: you might be missing a type parameter
[INFO] [stdout]     |
[INFO] [stdout] 544 | fn main() { #[allow(non_snake_case)] fn _doctest_main_src_lib_rs_544_0<int>() {
[INFO] [stdout]     |                                                                       +++++
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:547:21
[INFO] [stdout]     |
[INFO] [stdout] 547 |         |__VERUS_x: int| {
[INFO] [stdout]     |                     ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 547 -         |__VERUS_x: int| {
[INFO] [stdout] 547 +         |__VERUS_x: i32| {
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:549:19
[INFO] [stdout]     |
[INFO] [stdout] 549 |             Set::<int>::range(x, 20)
[INFO] [stdout]     |                   ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 549 -             Set::<int>::range(x, 20)
[INFO] [stdout] 549 +             Set::<i32>::range(x, 20)
[INFO] [stdout]     |
[INFO] [stdout] help: you might be missing a type parameter
[INFO] [stdout]     |
[INFO] [stdout] 544 | fn main() { #[allow(non_snake_case)] fn _doctest_main_src_lib_rs_544_0<int>() {
[INFO] [stdout]     |                                                                       +++++
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:550:29
[INFO] [stdout]     |
[INFO] [stdout] 550 |                 .filter(|y: int| (x + y != 25))
[INFO] [stdout]     |                             ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 550 -                 .filter(|y: int| (x + y != 25))
[INFO] [stdout] 550 +                 .filter(|y: i32| (x + y != 25))
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:552:25
[INFO] [stdout]     |
[INFO] [stdout] 552 |                     |y: int| ((x, y, y - x)),
[INFO] [stdout]     |                         ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 552 -                     |y: int| ((x, y, y - x)),
[INFO] [stdout] 552 +                     |y: i32| ((x, y, y - x)),
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:553:34
[INFO] [stdout]     |
[INFO] [stdout] 553 |                     |__VERUS_x: (int, int, int)| (__VERUS_x.1),
[INFO] [stdout]     |                                  ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 553 -                     |__VERUS_x: (int, int, int)| (__VERUS_x.1),
[INFO] [stdout] 553 +                     |__VERUS_x: (i32, int, int)| (__VERUS_x.1),
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:553:39
[INFO] [stdout]     |
[INFO] [stdout] 553 |                     |__VERUS_x: (int, int, int)| (__VERUS_x.1),
[INFO] [stdout]     |                                       ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 553 -                     |__VERUS_x: (int, int, int)| (__VERUS_x.1),
[INFO] [stdout] 553 +                     |__VERUS_x: (int, i32, int)| (__VERUS_x.1),
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:553:44
[INFO] [stdout]     |
[INFO] [stdout] 553 |                     |__VERUS_x: (int, int, int)| (__VERUS_x.1),
[INFO] [stdout]     |                                            ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 553 -                     |__VERUS_x: (int, int, int)| (__VERUS_x.1),
[INFO] [stdout] 553 +                     |__VERUS_x: (int, int, i32)| (__VERUS_x.1),
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:556:22
[INFO] [stdout]     |
[INFO] [stdout] 556 |         |__VERUS_x: (int, int, int)| __VERUS_x.0,
[INFO] [stdout]     |                      ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 556 -         |__VERUS_x: (int, int, int)| __VERUS_x.0,
[INFO] [stdout] 556 +         |__VERUS_x: (i32, int, int)| __VERUS_x.0,
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:556:27
[INFO] [stdout]     |
[INFO] [stdout] 556 |         |__VERUS_x: (int, int, int)| __VERUS_x.0,
[INFO] [stdout]     |                           ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 556 -         |__VERUS_x: (int, int, int)| __VERUS_x.0,
[INFO] [stdout] 556 +         |__VERUS_x: (int, i32, int)| __VERUS_x.0,
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:556:32
[INFO] [stdout]     |
[INFO] [stdout] 556 |         |__VERUS_x: (int, int, int)| __VERUS_x.0,
[INFO] [stdout]     |                                ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 556 -         |__VERUS_x: (int, int, int)| __VERUS_x.0,
[INFO] [stdout] 556 +         |__VERUS_x: (int, int, i32)| __VERUS_x.0,
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `Set` in this scope
[INFO] [stdout]    --> src/lib.rs:545:1
[INFO] [stdout]     |
[INFO] [stdout] 545 | Set::<int>::range(10, 20)
[INFO] [stdout]     | ^^^ use of undeclared type `Set`
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `Set` in this scope
[INFO] [stdout]    --> src/lib.rs:549:13
[INFO] [stdout]     |
[INFO] [stdout] 549 |             Set::<int>::range(x, 20)
[INFO] [stdout]     |             ^^^ use of undeclared type `Set`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 13 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0425, E0433.
[INFO] [stdout] For more information about an error, try `rustc --explain E0425`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/lib.rs - set_build (line 518) stdout ----
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:519:7
[INFO] [stdout]     |
[INFO] [stdout] 519 | Set::<int>::range(10, 20)
[INFO] [stdout]     |       ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 519 - Set::<int>::range(10, 20)
[INFO] [stdout] 519 + Set::<i32>::range(10, 20)
[INFO] [stdout]     |
[INFO] [stdout] help: you might be missing a type parameter
[INFO] [stdout]     |
[INFO] [stdout] 518 | fn main() { #[allow(non_snake_case)] fn _doctest_main_src_lib_rs_518_0<int>() {
[INFO] [stdout]     |                                                                       +++++
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:521:21
[INFO] [stdout]     |
[INFO] [stdout] 521 |         |__VERUS_x: int| {
[INFO] [stdout]     |                     ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 521 -         |__VERUS_x: int| {
[INFO] [stdout] 521 +         |__VERUS_x: i32| {
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:523:19
[INFO] [stdout]     |
[INFO] [stdout] 523 |             Set::<int>::range(0, 4096)
[INFO] [stdout]     |                   ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 523 -             Set::<int>::range(0, 4096)
[INFO] [stdout] 523 +             Set::<i32>::range(0, 4096)
[INFO] [stdout]     |
[INFO] [stdout] help: you might be missing a type parameter
[INFO] [stdout]     |
[INFO] [stdout] 518 | fn main() { #[allow(non_snake_case)] fn _doctest_main_src_lib_rs_518_0<int>() {
[INFO] [stdout]     |                                                                       +++++
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `int` in this scope
[INFO] [stdout]    --> src/lib.rs:525:30
[INFO] [stdout]     |
[INFO] [stdout] 525 |                     |offset: int| (Address { page, offset }),
[INFO] [stdout]     |                              ^^^ not found in this scope
[INFO] [stdout]     |
[INFO] [stdout] help: you might have intended to use the `i32` primitive type
[INFO] [stdout]     |
[INFO] [stdout] 525 -                     |offset: int| (Address { page, offset }),
[INFO] [stdout] 525 +                     |offset: i32| (Address { page, offset }),
[INFO] [stdout]     |
[INFO] [stdout] 
[INFO] [stdout] error[E0422]: cannot find struct, variant or union type `Address` in this scope
[INFO] [stdout]    --> src/lib.rs:525:36
[INFO] [stdout]     |
[INFO] [stdout] 525 |                     |offset: int| (Address { page, offset }),
[INFO] [stdout]     |                                    ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `Address` in this scope
[INFO] [stdout]    --> src/lib.rs:526:33
[INFO] [stdout]     |
[INFO] [stdout] 526 |                     |__VERUS_x: Address| (__VERUS_x.offset),
[INFO] [stdout]     |                                 ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0425]: cannot find type `Address` in this scope
[INFO] [stdout]    --> src/lib.rs:529:21
[INFO] [stdout]     |
[INFO] [stdout] 529 |         |__VERUS_x: Address| __VERUS_x.page,
[INFO] [stdout]     |                     ^^^^^^^ not found in this scope
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `Set` in this scope
[INFO] [stdout]    --> src/lib.rs:519:1
[INFO] [stdout]     |
[INFO] [stdout] 519 | Set::<int>::range(10, 20)
[INFO] [stdout]     | ^^^ use of undeclared type `Set`
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find type `Set` in this scope
[INFO] [stdout]    --> src/lib.rs:523:13
[INFO] [stdout]     |
[INFO] [stdout] 523 |             Set::<int>::range(0, 4096)
[INFO] [stdout]     |             ^^^ use of undeclared type `Set`
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 9 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0422, E0425, E0433.
[INFO] [stdout] For more information about an error, try `rustc --explain E0422`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/unerased_proxies.rs - unerased_proxies (line 17) stdout ----
[INFO] [stdout] error[E0423]: cannot find function `assert` in this scope
[INFO] [stdout]   --> src/unerased_proxies.rs:19:4
[INFO] [stdout]    |
[INFO] [stdout] 19 |    assert(true);
[INFO] [stdout]    |    ^^^^^^ not found in this scope
[INFO] [stdout]    |
[INFO] [stdout]    = note: a macro named `assert` exists in another namespace
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]    |
[INFO] [stdout] 19 |    assert!(true);
[INFO] [stdout]    |          +
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 1 previous error
[INFO] [stdout] 
[INFO] [stdout] For more information about this error, try `rustc --explain E0423`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] ---- src/unerased_proxies.rs - unerased_proxies (line 26) stdout ----
[INFO] [stdout] error[E0433]: cannot find module or crate `verifier` in this scope
[INFO] [stdout]   --> src/unerased_proxies.rs:34:3
[INFO] [stdout]    |
[INFO] [stdout] 34 | #[verifier::external]
[INFO] [stdout]    |   ^^^^^^^^ use of unresolved module or unlinked crate `verifier`
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find module or crate `verus` in this scope
[INFO] [stdout]   --> src/unerased_proxies.rs:35:3
[INFO] [stdout]    |
[INFO] [stdout] 35 | #[verus::internal(has_unerased_proxy)]
[INFO] [stdout]    |   ^^^^^ use of unresolved module or unlinked crate `verus`
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find module or crate `verus` in this scope
[INFO] [stdout]   --> src/unerased_proxies.rs:27:3
[INFO] [stdout]    |
[INFO] [stdout] 27 | #[verus::internal(unerased_proxy)]
[INFO] [stdout]    |   ^^^^^ use of unresolved module or unlinked crate `verus`
[INFO] [stdout] 
[INFO] [stdout] error[E0433]: cannot find module or crate `verus` in this scope
[INFO] [stdout]   --> src/unerased_proxies.rs:28:3
[INFO] [stdout]    |
[INFO] [stdout] 28 | #[verus::internal(encoded_const)]
[INFO] [stdout]    |   ^^^^^ use of unresolved module or unlinked crate `verus`
[INFO] [stdout] 
[INFO] [stdout] error[E0423]: cannot find function `assert` in this scope
[INFO] [stdout]   --> src/unerased_proxies.rs:30:4
[INFO] [stdout]    |
[INFO] [stdout] 30 |    assert(true);
[INFO] [stdout]    |    ^^^^^^ not found in this scope
[INFO] [stdout]    |
[INFO] [stdout]    = note: a macro named `assert` exists in another namespace
[INFO] [stdout] help: use `!` to invoke the macro
[INFO] [stdout]    |
[INFO] [stdout] 30 |    assert!(true);
[INFO] [stdout]    |          +
[INFO] [stdout] 
[INFO] [stdout] error: aborting due to 5 previous errors
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0423, E0433.
[INFO] [stdout] For more information about an error, try `rustc --explain E0423`.
[INFO] [stdout] Couldn't compile the test.
[INFO] [stdout] 
[INFO] [stdout] failures:
[INFO] [stdout]     src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 919)
[INFO] [stdout]     src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 927)
[INFO] [stdout]     src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 933)
[INFO] [stdout]     src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 944)
[INFO] [stdout]     src/attr_rewrite.rs - attr_rewrite::rewrite_verus_spec_on_expr_local (line 949)
[INFO] [stdout]     src/contrib/spec_derive.rs - contrib::spec_derive::make_spec_type (line 26)
[INFO] [stdout]     src/contrib/spec_derive.rs - contrib::spec_derive::self_view (line 580)
[INFO] [stdout]     src/lib.rs - set_build (line 441)
[INFO] [stdout]     src/lib.rs - set_build (line 453)
[INFO] [stdout]     src/lib.rs - set_build (line 460)
[INFO] [stdout]     src/lib.rs - set_build (line 467)
[INFO] [stdout]     src/lib.rs - set_build (line 472)
[INFO] [stdout]     src/lib.rs - set_build (line 478)
[INFO] [stdout]     src/lib.rs - set_build (line 485)
[INFO] [stdout]     src/lib.rs - set_build (line 492)
[INFO] [stdout]     src/lib.rs - set_build (line 498)
[INFO] [stdout]     src/lib.rs - set_build (line 518)
[INFO] [stdout]     src/lib.rs - set_build (line 534)
[INFO] [stdout]     src/lib.rs - set_build (line 544)
[INFO] [stdout]     src/unerased_proxies.rs - unerased_proxies (line 17)
[INFO] [stdout]     src/unerased_proxies.rs - unerased_proxies (line 26)
[INFO] [stdout]     src/unerased_proxies.rs - unerased_proxies (line 43)
[INFO] [stdout]     src/unerased_proxies.rs - unerased_proxies (line 52)
[INFO] [stdout] 
[INFO] [stdout] test result: FAILED. 0 passed; 23 failed; 5 ignored; 0 measured; 0 filtered out; finished in 0.39s
[INFO] [stdout] 
[INFO] [stderr] error: doctest failed, to rerun pass `--doc`
[INFO] running `Command { std: "docker" "inspect" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "rm" "-f" "709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95", kill_on_drop: false }`
[INFO] [stdout] 709c5299c86d4f5cf04d58a28169225cf80f49a82132e35675c1b6f4c7002a95
