[INFO] fetching crate ravencheck 0.3.0... [INFO] testing ravencheck-0.3.0 against try#b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b for pr-145330-1 [INFO] extracting crate ravencheck 0.3.0 into /workspace/builds/worker-7-tc2/source [INFO] started tweaking crates.io crate ravencheck 0.3.0 [INFO] removed 0 missing examples [INFO] finished tweaking crates.io crate ravencheck 0.3.0 [INFO] tweaked toml for crates.io crate ravencheck 0.3.0 written to /workspace/builds/worker-7-tc2/source/Cargo.toml [INFO] validating manifest of crates.io crate ravencheck 0.3.0 on toolchain b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b [INFO] running `Command { std: CARGO_HOME="/workspace/cargo-home" RUSTUP_HOME="/workspace/rustup-home" "/workspace/cargo-home/bin/cargo" "+b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b" "metadata" "--manifest-path" "Cargo.toml" "--no-deps", kill_on_drop: false }` [INFO] crate crates.io crate ravencheck 0.3.0 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" "+b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b" "fetch" "--manifest-path" "Cargo.toml", kill_on_drop: false }` [INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc2/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc2/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:e90291280db7d1fac5b66fc6dad9f9662629e7365a55743daf9bdf73ebc4ea79" "/opt/rustwide/cargo-home/bin/cargo" "+b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b" "metadata" "--no-deps" "--format-version=1", kill_on_drop: false }` [INFO] [stdout] 8283e2a60d05a44e62215f9de764db6c3a9ad81911d7cfd2989932865c484235 [INFO] running `Command { std: "docker" "start" "-a" "8283e2a60d05a44e62215f9de764db6c3a9ad81911d7cfd2989932865c484235", kill_on_drop: false }` [INFO] running `Command { std: "docker" "inspect" "8283e2a60d05a44e62215f9de764db6c3a9ad81911d7cfd2989932865c484235", kill_on_drop: false }` [INFO] running `Command { std: "docker" "rm" "-f" "8283e2a60d05a44e62215f9de764db6c3a9ad81911d7cfd2989932865c484235", kill_on_drop: false }` [INFO] [stdout] 8283e2a60d05a44e62215f9de764db6c3a9ad81911d7cfd2989932865c484235 [INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc2/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc2/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=forbid" "-e" "RUSTDOCFLAGS=--cap-lints=forbid" "-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:e90291280db7d1fac5b66fc6dad9f9662629e7365a55743daf9bdf73ebc4ea79" "/opt/rustwide/cargo-home/bin/cargo" "+b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b" "build" "--frozen" "--message-format=json", kill_on_drop: false }` [INFO] [stdout] 1888c5df993c6a969cfb7b12e063aea32397f51ed2fe61fc3213b999198f2d29 [INFO] running `Command { std: "docker" "start" "-a" "1888c5df993c6a969cfb7b12e063aea32397f51ed2fe61fc3213b999198f2d29", kill_on_drop: false }` [INFO] [stderr] Compiling unicode-ident v1.0.18 [INFO] [stderr] Compiling fixedbitset v0.5.7 [INFO] [stderr] Compiling libc v0.2.175 [INFO] [stderr] Compiling aho-corasick v1.1.3 [INFO] [stderr] Compiling proc-macro2 v1.0.101 [INFO] [stderr] Compiling ahash v0.8.12 [INFO] [stderr] Compiling getrandom v0.3.3 [INFO] [stderr] Compiling hashbrown v0.15.5 [INFO] [stderr] Compiling anstyle-parse v0.2.7 [INFO] [stderr] Compiling anstyle-query v1.1.4 [INFO] [stderr] Compiling colorchoice v1.0.4 [INFO] [stderr] Compiling anstyle v1.0.11 [INFO] [stderr] Compiling jiff v0.2.15 [INFO] [stderr] Compiling easy-smt v0.2.8 [INFO] [stderr] Compiling anstream v0.6.20 [INFO] [stderr] Compiling quote v1.0.40 [INFO] [stderr] Compiling syn v2.0.106 [INFO] [stderr] Compiling regex-automata v0.4.9 [INFO] [stderr] Compiling indexmap v2.10.0 [INFO] [stderr] Compiling petgraph v0.8.2 [INFO] [stderr] Compiling regex v1.11.1 [INFO] [stderr] Compiling graph-cycles v0.3.0 [INFO] [stderr] Compiling env_filter v0.1.3 [INFO] [stderr] Compiling env_logger v0.11.8 [INFO] [stderr] Compiling ravenlang v0.3.0 [INFO] [stderr] Compiling ravencheck-macros v0.3.0 [INFO] [stderr] Compiling ravencheck v0.3.0 (/opt/rustwide/workdir) [INFO] [stderr] Finished `dev` profile [unoptimized + debuginfo] target(s) in 17.17s [INFO] running `Command { std: "docker" "inspect" "1888c5df993c6a969cfb7b12e063aea32397f51ed2fe61fc3213b999198f2d29", kill_on_drop: false }` [INFO] running `Command { std: "docker" "rm" "-f" "1888c5df993c6a969cfb7b12e063aea32397f51ed2fe61fc3213b999198f2d29", kill_on_drop: false }` [INFO] [stdout] 1888c5df993c6a969cfb7b12e063aea32397f51ed2fe61fc3213b999198f2d29 [INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc2/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc2/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=forbid" "-e" "RUSTDOCFLAGS=--cap-lints=forbid" "-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:e90291280db7d1fac5b66fc6dad9f9662629e7365a55743daf9bdf73ebc4ea79" "/opt/rustwide/cargo-home/bin/cargo" "+b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b" "test" "--frozen" "--no-run" "--message-format=json", kill_on_drop: false }` [INFO] [stdout] a5ce0604bf0fa24e644152e625107576d3a250e90cb6f3f28c3d0ef33c7c2ce9 [INFO] running `Command { std: "docker" "start" "-a" "a5ce0604bf0fa24e644152e625107576d3a250e90cb6f3f28c3d0ef33c7c2ce9", kill_on_drop: false }` [INFO] [stderr] Compiling ravencheck v0.3.0 (/opt/rustwide/workdir) [INFO] [stderr] Finished `test` profile [unoptimized + debuginfo] target(s) in 1.32s [INFO] running `Command { std: "docker" "inspect" "a5ce0604bf0fa24e644152e625107576d3a250e90cb6f3f28c3d0ef33c7c2ce9", kill_on_drop: false }` [INFO] running `Command { std: "docker" "rm" "-f" "a5ce0604bf0fa24e644152e625107576d3a250e90cb6f3f28c3d0ef33c7c2ce9", kill_on_drop: false }` [INFO] [stdout] a5ce0604bf0fa24e644152e625107576d3a250e90cb6f3f28c3d0ef33c7c2ce9 [INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc2/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc2/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=forbid" "-e" "RUSTDOCFLAGS=--cap-lints=forbid" "-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:e90291280db7d1fac5b66fc6dad9f9662629e7365a55743daf9bdf73ebc4ea79" "/opt/rustwide/cargo-home/bin/cargo" "+b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b" "test" "--frozen", kill_on_drop: false }` [INFO] [stdout] a4824732bc49136f42d9736f8665808c96f09e90fd461193b135ffab4c4e6a75 [INFO] running `Command { std: "docker" "start" "-a" "a4824732bc49136f42d9736f8665808c96f09e90fd461193b135ffab4c4e6a75", kill_on_drop: false }` [INFO] [stderr] Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s [INFO] [stderr] Running unittests src/lib.rs (/opt/rustwide/target/debug/deps/ravencheck-4246cd4a22c3dc75) [INFO] [stdout] [INFO] [stdout] running 20 tests [INFO] [stdout] test macro_examples::filter::my_mod::filter_test ... ok [INFO] [stdout] test macro_examples::main_example_set::my_mod::normal_tests::union_empty_set ... ok [INFO] [stdout] test macro_examples::main_example_set::my_mod::normal_tests::empty_is_empty ... ok [INFO] [stdout] test macro_examples::sets::my_mod::runtime_properties::union_empty_set ... ok [INFO] [stdout] test macro_examples::sets::my_mod::runtime_properties::empty_is_empty ... ok [INFO] [stdout] test macro_examples::sets_using_alias::my_mod::normal_tests::empty_is_empty ... ok [INFO] [stdout] test macro_examples::sets_using_alias::my_mod::normal_tests::union_empty_set ... ok [INFO] [stdout] test macro_examples::filter::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::recursive::rvn::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::minimal_polymorphic::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::minimal::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::main_example_set::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::sets::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::minimal_filter::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::type_parameter_sets::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::sets_using_alias::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::import_test::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::nat::my_nat_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::main_example_nat::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] test macro_examples::nat_u32::my_mod::ravencheck_tests::check_properties ... FAILED [INFO] [stdout] [INFO] [stdout] failures: [INFO] [stdout] [INFO] [stdout] ---- macro_examples::filter::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [] [INFO] [stdout] Expanding call filter... [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("u32", []))), (Manual("s"), Base(UI("MySet", [])))], Bind1(LogQuantifier(Exists, [(Auto(18), Base(UI("MySet", [])))], Bind1(LogQuantifier(Forall, [(Auto(29), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(29), []), Var(Auto(18), [])]), Auto(56), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(29), []), Var(Manual("s"), [])]), Auto(57), Bind1(Eq(false, [Var(Auto(29), [])], [Var(Manual("e"), [])]), Auto(9), Bind1(LogOpN(And, [Var(Auto(9), []), Var(Auto(57), [])]), Auto(41), Bind1(Eq(true, [Var(Auto(56), [])], [Var(Auto(41), [])]), Auto(75), Return([Var(Auto(75), [])]))))))), Auto(70), Bind1(Eq(false, [Var(Manual("s"), [])], [Var(Auto(18), [])]), Auto(71), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, false), [Var(Manual("e"), []), Var(Manual("s"), [])]), Auto(72), Bind1(LogOpN(And, [Var(Auto(71), []), Var(Auto(72), [])]), Auto(69), Bind1(LogOpN(And, [Var(Auto(69), []), Var(Auto(70), [])]), Auto(68), Return([Var(Auto(68), [])]))))))), Auto(65), Return([Var(Auto(65), [])]))), Auto(62), Return([Var(Auto(62), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("MySet", []))), (Manual("b"), Base(UI("MySet", [])))], Bind1(Eq(true, [Var(Manual("a"), [])], [Var(Manual("b"), [])]), Auto(13), Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("a"), [])]), Auto(17), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("b"), [])]), Auto(18), Bind1(Eq(false, [Var(Auto(17), [])], [Var(Auto(18), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Bind1(LogOpN(Or, [Var(Auto(1), []), Var(Auto(13), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::filter::my_mod::ravencheck_tests::check_properties' (26) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb310a6d - ravencheck::macro_examples::filter::my_mod::ravencheck_tests::check_properties::hd34f1eb81acb1846 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/filter.rs:1:1 [INFO] [stdout] 25: 0x5d4feb310ab7 - ravencheck::macro_examples::filter::my_mod::ravencheck_tests::check_properties::{{closure}}::h0583009311fdf0eb [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/filter.rs:1:30 [INFO] [stdout] 26: 0x5d4feb30ec26 - core::ops::function::FnOnce::call_once::hd76eb32a0cbae199 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::recursive::rvn::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Expanding call cons::... [INFO] [stdout] Expanding call cons::... [INFO] [stdout] Expanding call cons::... [INFO] [stdout] Expanding call cons::... [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("E", []))), (Manual("l"), Base(UI("List", [Base(UI("E", []))])))], Bind1(LogQuantifier(Exists, [(Auto(22), Base(UI("List", [Base(UI("E", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "cons", types: [Base(UI("E", []))] }, true), [Var(Manual("e"), []), Var(Manual("l"), []), Var(Auto(22), [])]), Auto(101), Bind1(LogQuantifier(Exists, [(Auto(23), Base(UI("List", [Base(UI("E", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "cons", types: [Base(UI("E", []))] }, true), [Var(Manual("e"), []), Var(Auto(22), []), Var(Auto(23), [])]), Auto(99), Bind1(LogQuantifier(Exists, [(Auto(24), Base(UI("List", [Base(UI("E", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "cons", types: [Base(UI("E", []))] }, true), [Var(Manual("e"), []), Var(Manual("l"), []), Var(Auto(24), [])]), Auto(97), Bind1(LogQuantifier(Exists, [(Auto(25), Base(UI("List", [Base(UI("E", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "cons", types: [Base(UI("E", []))] }, true), [Var(Manual("e"), []), Var(Auto(24), []), Var(Auto(25), [])]), Auto(95), Bind1(Eq(false, [Var(Auto(23), [])], [Var(Auto(25), [])]), Auto(100), Bind1(LogOpN(And, [Var(Auto(100), []), Var(Auto(101), [])]), Auto(98), Bind1(LogOpN(And, [Var(Auto(98), []), Var(Auto(99), [])]), Auto(96), Bind1(LogOpN(And, [Var(Auto(96), []), Var(Auto(97), [])]), Auto(94), Bind1(LogOpN(And, [Var(Auto(94), []), Var(Auto(95), [])]), Auto(93), Return([Var(Auto(93), [])])))))))), Auto(90), Return([Var(Auto(90), [])])))), Auto(87), Return([Var(Auto(87), [])])))), Auto(84), Return([Var(Auto(84), [])])))), Auto(81), Return([Var(Auto(81), [])]))), Auto(78), Return([Var(Auto(78), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::recursive::rvn::ravencheck_tests::check_properties' (37) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb30d52b - ravencheck::macro_examples::recursive::rvn::ravencheck_tests::check_properties::h534f2a22c67fd1da [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/recursive.rs:1:1 [INFO] [stdout] 25: 0x5d4feb30d287 - ravencheck::macro_examples::recursive::rvn::ravencheck_tests::check_properties::{{closure}}::ha14f6058ea23a870 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/recursive.rs:1:30 [INFO] [stdout] 26: 0x5d4feb30fe06 - core::ops::function::FnOnce::call_once::h8f25ca8d2cf7b192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::minimal_polymorphic::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [InstRule { left: UI("HashSet", [Base(UI("E", []))]), right: [Base(UI("E", []))] }] [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Manual("a"), Base(UI("HashSet", [Base(UI("E", []))]))), (Manual("b"), Base(UI("HashSet", [Base(UI("E", []))])))], Bind1(Eq(false, [Var(Manual("a"), [])], [Var(Manual("b"), [])]), Auto(7), Return([Var(Auto(7), [])]))), Auto(4), Return([Var(Auto(4), [])])) [INFO] [stdout] Matching HashSet with HashSet [INFO] [stdout] Subbing types [Base(UI("E", []))] for ["E"] [INFO] [stdout] Inst axiom body: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("HashSet", [Base(UI("E", []))]))), (Manual("b"), Base(UI("HashSet", [Base(UI("E", []))])))], BindN(Seq(BindN(Seq(Return([Var(Manual("a"), [])])), [Atom(Auto(11))], BindN(Seq(Return([Var(Manual("b"), [])])), [Atom(Auto(12))], Bind1(Eq(true, [Var(Auto(11), [])], [Var(Auto(12), [])]), Auto(13), Return([Var(Auto(13), [])]))))), [Atom(Auto(15))], BindN(Seq(Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("E", [])))], BindN(Seq(BindN(Seq(Return([Var(Manual("a"), [])])), [Atom(Auto(3))], BindN(Seq(Return([Var(Manual("e"), [])])), [Atom(Auto(2))], Apply(BindN(Seq(Return([Var(Manual("member"), [Base(UI("E", []))])])), [Atom(Auto(4))], Force(Var(Auto(4), []))), [], [Var(Auto(2), []), Var(Auto(3), [])])))), [Atom(Auto(5))], BindN(Seq(BindN(Seq(Return([Var(Manual("b"), [])])), [Atom(Auto(7))], BindN(Seq(Return([Var(Manual("e"), [])])), [Atom(Auto(6))], Apply(BindN(Seq(Return([Var(Manual("member"), [Base(UI("E", []))])])), [Atom(Auto(8))], Force(Var(Auto(8), []))), [], [Var(Auto(6), []), Var(Auto(7), [])])))), [Atom(Auto(9))], Bind1(Eq(false, [Var(Auto(5), [])], [Var(Auto(9), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Return([Var(Auto(1), [])]))), [Atom(Auto(14))], Bind1(LogOpN(Or, [Var(Auto(14), []), Var(Auto(15), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("HashSet", [Base(UI("E", []))]))), (Manual("b"), Base(UI("HashSet", [Base(UI("E", []))])))], Bind1(Eq(true, [Var(Manual("a"), [])], [Var(Manual("b"), [])]), Auto(13), Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("E", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [Base(UI("E", []))] }, true), [Var(Manual("e"), []), Var(Manual("a"), [])]), Auto(17), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [Base(UI("E", []))] }, true), [Var(Manual("e"), []), Var(Manual("b"), [])]), Auto(18), Bind1(Eq(false, [Var(Auto(17), [])], [Var(Auto(18), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Bind1(LogOpN(Or, [Var(Auto(1), []), Var(Auto(13), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::minimal_polymorphic::my_mod::ravencheck_tests::check_properties' (34) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb304ef9 - ravencheck::macro_examples::minimal_polymorphic::my_mod::ravencheck_tests::check_properties::h7ef26304cca9da25 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/minimal_polymorphic.rs:1:1 [INFO] [stdout] 25: 0x5d4feb304f47 - ravencheck::macro_examples::minimal_polymorphic::my_mod::ravencheck_tests::check_properties::{{closure}}::h08e433b9768f0a4c [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/minimal_polymorphic.rs:1:30 [INFO] [stdout] 26: 0x5d4feb30ef16 - core::ops::function::FnOnce::call_once::h360d71dde91da578 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::minimal::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [] [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Manual("a"), Base(UI("Set", []))), (Manual("b"), Base(UI("Set", [])))], Bind1(Eq(false, [Var(Manual("a"), [])], [Var(Manual("b"), [])]), Auto(7), Return([Var(Auto(7), [])]))), Auto(4), Return([Var(Auto(4), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("Set", []))), (Manual("b"), Base(UI("Set", [])))], Bind1(Eq(true, [Var(Manual("a"), [])], [Var(Manual("b"), [])]), Auto(13), Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("Elem", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("a"), [])]), Auto(17), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("b"), [])]), Auto(18), Bind1(Eq(false, [Var(Auto(17), [])], [Var(Auto(18), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Bind1(LogOpN(Or, [Var(Auto(1), []), Var(Auto(13), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::minimal::my_mod::ravencheck_tests::check_properties' (32) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb306946 - ravencheck::macro_examples::minimal::my_mod::ravencheck_tests::check_properties::h03f4e15c468b9f20 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/minimal.rs:1:1 [INFO] [stdout] 25: 0x5d4feb306997 - ravencheck::macro_examples::minimal::my_mod::ravencheck_tests::check_properties::{{closure}}::hac72fa55e592b7ea [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/minimal.rs:1:30 [INFO] [stdout] 26: 0x5d4feb30fe46 - core::ops::function::FnOnce::call_once::hadd596ce305c015c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::main_example_set::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [] [INFO] [stdout] Pushing axiom with rules [] [INFO] [stdout] Expanding call union... [INFO] [stdout] Expanding call union... [INFO] [stdout] Expanding call union... [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Manual("a"), Base(UI("MySet", []))), (Manual("b"), Base(UI("MySet", [])))], Bind1(LogQuantifier(Exists, [(Auto(13), Base(UI("MySet", [])))], Bind1(LogOpN(Pred(OpCode { ident: "union", types: [] }, true), [Var(Manual("a"), []), Var(Manual("b"), []), Var(Auto(13), [])]), Auto(172), Bind1(LogQuantifier(Forall, [(Auto(16), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(16), []), Var(Auto(13), [])]), Auto(53), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(16), []), Var(Manual("a"), [])]), Auto(54), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(16), []), Var(Manual("b"), [])]), Auto(55), Bind1(LogOpN(Or, [Var(Auto(55), []), Var(Auto(54), [])]), Auto(29), Bind1(Eq(true, [Var(Auto(53), [])], [Var(Auto(29), [])]), Auto(181), Return([Var(Auto(181), [])]))))))), Auto(171), Bind1(LogQuantifier(Exists, [(Auto(14), Base(UI("MySet", [])))], Bind1(LogOpN(Pred(OpCode { ident: "union", types: [] }, true), [Var(Auto(13), []), Var(Manual("b"), []), Var(Auto(14), [])]), Auto(169), Bind1(LogQuantifier(Forall, [(Auto(61), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(61), []), Var(Auto(14), [])]), Auto(98), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(61), []), Var(Auto(13), [])]), Auto(99), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(61), []), Var(Manual("b"), [])]), Auto(100), Bind1(LogOpN(Or, [Var(Auto(100), []), Var(Auto(99), [])]), Auto(74), Bind1(Eq(true, [Var(Auto(98), [])], [Var(Auto(74), [])]), Auto(178), Return([Var(Auto(178), [])]))))))), Auto(168), Bind1(LogQuantifier(Exists, [(Auto(15), Base(UI("MySet", [])))], Bind1(LogOpN(Pred(OpCode { ident: "union", types: [] }, true), [Var(Manual("a"), []), Var(Manual("b"), []), Var(Auto(15), [])]), Auto(166), Bind1(LogQuantifier(Forall, [(Auto(106), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(106), []), Var(Auto(15), [])]), Auto(143), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(106), []), Var(Manual("a"), [])]), Auto(144), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(106), []), Var(Manual("b"), [])]), Auto(145), Bind1(LogOpN(Or, [Var(Auto(145), []), Var(Auto(144), [])]), Auto(119), Bind1(Eq(true, [Var(Auto(143), [])], [Var(Auto(119), [])]), Auto(175), Return([Var(Auto(175), [])]))))))), Auto(165), Bind1(Eq(false, [Var(Auto(14), [])], [Var(Auto(15), [])]), Auto(170), Bind1(LogOpN(And, [Var(Auto(170), []), Var(Auto(171), []), Var(Auto(172), [])]), Auto(167), Bind1(LogOpN(And, [Var(Auto(167), []), Var(Auto(168), []), Var(Auto(169), [])]), Auto(164), Bind1(LogOpN(And, [Var(Auto(164), []), Var(Auto(165), []), Var(Auto(166), [])]), Auto(163), Return([Var(Auto(163), [])])))))))), Auto(160), Return([Var(Auto(160), [])]))))), Auto(157), Return([Var(Auto(157), [])]))))), Auto(154), Return([Var(Auto(154), [])]))), Auto(151), Return([Var(Auto(151), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("MySet", []))), (Manual("b"), Base(UI("MySet", [])))], Bind1(Eq(true, [Var(Manual("a"), [])], [Var(Manual("b"), [])]), Auto(13), Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("a"), [])]), Auto(17), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("b"), [])]), Auto(18), Bind1(Eq(false, [Var(Auto(17), [])], [Var(Auto(18), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Bind1(LogOpN(Or, [Var(Auto(1), []), Var(Auto(13), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("e"), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, false), [Var(Manual("e"), []), OpCode(ZeroArgAsConst, OpCode { ident: "empty_set", types: [] })]), Auto(8), Return([Var(Auto(8), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::main_example_set::my_mod::ravencheck_tests::check_properties' (31) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb310798 - ravencheck::macro_examples::main_example_set::my_mod::ravencheck_tests::check_properties::h2bec40686f1184d2 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/main_example_set.rs:11:1 [INFO] [stdout] 25: 0x5d4feb310567 - ravencheck::macro_examples::main_example_set::my_mod::ravencheck_tests::check_properties::{{closure}}::h71c16c84ae8a2300 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/main_example_set.rs:11:30 [INFO] [stdout] 26: 0x5d4feb30fda6 - core::ops::function::FnOnce::call_once::h6062062811c42563 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::sets::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [] [INFO] [stdout] Pushing axiom with rules [] [INFO] [stdout] Expanding call union... [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("Elem", []))), (Manual("s"), Base(UI("Set", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("s"), [])]), Auto(75), Bind1(LogQuantifier(Exists, [(Auto(16), Base(UI("Set", [])))], Bind1(LogOpN(Pred(OpCode { ident: "union", types: [] }, true), [Var(Manual("s"), []), Var(Manual("s"), []), Var(Auto(16), [])]), Auto(73), Bind1(LogQuantifier(Forall, [(Auto(19), Base(UI("Elem", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(19), []), Var(Auto(16), [])]), Auto(56), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(19), []), Var(Manual("s"), [])]), Auto(57), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(19), []), Var(Manual("s"), [])]), Auto(58), Bind1(LogOpN(Or, [Var(Auto(58), []), Var(Auto(57), [])]), Auto(32), Bind1(Eq(true, [Var(Auto(56), [])], [Var(Auto(32), [])]), Auto(78), Return([Var(Auto(78), [])]))))))), Auto(72), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, false), [Var(Manual("e"), []), Var(Auto(16), [])]), Auto(74), Bind1(LogOpN(And, [Var(Auto(74), []), Var(Auto(75), [])]), Auto(71), Bind1(LogOpN(And, [Var(Auto(71), []), Var(Auto(72), []), Var(Auto(73), [])]), Auto(70), Return([Var(Auto(70), [])]))))))), Auto(67), Return([Var(Auto(67), [])])))), Auto(64), Return([Var(Auto(64), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("Set", []))), (Manual("b"), Base(UI("Set", [])))], Bind1(Eq(true, [Var(Manual("a"), [])], [Var(Manual("b"), [])]), Auto(13), Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("Elem", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("a"), [])]), Auto(17), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("b"), [])]), Auto(18), Bind1(Eq(false, [Var(Auto(17), [])], [Var(Auto(18), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Bind1(LogOpN(Or, [Var(Auto(1), []), Var(Auto(13), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("e"), Base(UI("Elem", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, false), [Var(Manual("e"), []), OpCode(ZeroArgAsConst, OpCode { ident: "empty_set", types: [] })]), Auto(8), Return([Var(Auto(8), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::sets::my_mod::ravencheck_tests::check_properties' (38) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb30e713 - ravencheck::macro_examples::sets::my_mod::ravencheck_tests::check_properties::h0dbe7ab4f54f2b6d [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/sets.rs:14:1 [INFO] [stdout] 25: 0x5d4feb30e557 - ravencheck::macro_examples::sets::my_mod::ravencheck_tests::check_properties::{{closure}}::h08a826dc342a0b65 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/sets.rs:14:30 [INFO] [stdout] 26: 0x5d4feb30f456 - core::ops::function::FnOnce::call_once::ha41f9e43ff5ae778 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::minimal_filter::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [InstRule { left: UI("HashSet", [Base(UI("E", []))]), right: [Base(UI("E", []))] }] [INFO] [stdout] Pushing axiom with rules [InstRule { left: UI("HashSet", [Base(UI("E", []))]), right: [Base(UI("E", []))] }] [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Manual("a"), Base(UI("HashSet", [Base(UI("E", []))]))), (Manual("b"), Base(UI("HashSet", [Base(UI("E", []))])))], Bind1(Eq(false, [Var(Manual("a"), [])], [Var(Manual("b"), [])]), Auto(7), Return([Var(Auto(7), [])]))), Auto(4), Return([Var(Auto(4), [])])) [INFO] [stdout] Matching HashSet with HashSet [INFO] [stdout] Subbing types [Base(UI("E", []))] for ["E"] [INFO] [stdout] Inst axiom body: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("HashSet", [Base(UI("E", []))]))), (Manual("b"), Base(UI("HashSet", [Base(UI("E", []))])))], BindN(Seq(BindN(Seq(Return([Var(Manual("a"), [])])), [Atom(Auto(11))], BindN(Seq(Return([Var(Manual("b"), [])])), [Atom(Auto(12))], Bind1(Eq(true, [Var(Auto(11), [])], [Var(Auto(12), [])]), Auto(13), Return([Var(Auto(13), [])]))))), [Atom(Auto(15))], BindN(Seq(Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("E", [])))], BindN(Seq(BindN(Seq(Return([Var(Manual("a"), [])])), [Atom(Auto(3))], BindN(Seq(Return([Var(Manual("e"), [])])), [Atom(Auto(2))], Apply(BindN(Seq(Return([Var(Manual("member"), [Base(UI("E", []))])])), [Atom(Auto(4))], Force(Var(Auto(4), []))), [], [Var(Auto(2), []), Var(Auto(3), [])])))), [Atom(Auto(5))], BindN(Seq(BindN(Seq(Return([Var(Manual("b"), [])])), [Atom(Auto(7))], BindN(Seq(Return([Var(Manual("e"), [])])), [Atom(Auto(6))], Apply(BindN(Seq(Return([Var(Manual("member"), [Base(UI("E", []))])])), [Atom(Auto(8))], Force(Var(Auto(8), []))), [], [Var(Auto(6), []), Var(Auto(7), [])])))), [Atom(Auto(9))], Bind1(Eq(false, [Var(Auto(5), [])], [Var(Auto(9), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Return([Var(Auto(1), [])]))), [Atom(Auto(14))], Bind1(LogOpN(Or, [Var(Auto(14), []), Var(Auto(15), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] Matching HashSet with HashSet [INFO] [stdout] Subbing types [Base(UI("E", []))] for ["E"] [INFO] [stdout] Inst axiom body: Bind1(LogQuantifier(Forall, [(Manual("e"), Base(UI("E", [])))], BindN(Seq(BindN(Seq(Apply(BindN(Seq(Return([Var(Manual("set_empty"), [Base(UI("E", []))])])), [Atom(Auto(1))], Force(Var(Auto(1), []))), [], [])), [Atom(Auto(3))], BindN(Seq(Return([Var(Manual("e"), [])])), [Atom(Auto(2))], Apply(BindN(Seq(Return([Var(Manual("member"), [Base(UI("E", []))])])), [Atom(Auto(4))], Force(Var(Auto(4), []))), [], [Var(Auto(2), []), Var(Auto(3), [])])))), [Atom(Auto(5))], Bind1(LogNot(Var(Auto(5), [])), Auto(6), Return([Var(Auto(6), [])])))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("HashSet", [Base(UI("E", []))]))), (Manual("b"), Base(UI("HashSet", [Base(UI("E", []))])))], Bind1(Eq(true, [Var(Manual("a"), [])], [Var(Manual("b"), [])]), Auto(13), Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("E", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [Base(UI("E", []))] }, true), [Var(Manual("e"), []), Var(Manual("a"), [])]), Auto(17), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [Base(UI("E", []))] }, true), [Var(Manual("e"), []), Var(Manual("b"), [])]), Auto(18), Bind1(Eq(false, [Var(Auto(17), [])], [Var(Auto(18), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Bind1(LogOpN(Or, [Var(Auto(1), []), Var(Auto(13), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("e"), Base(UI("E", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [Base(UI("E", []))] }, false), [Var(Manual("e"), []), OpCode(ZeroArgAsConst, OpCode { ident: "set_empty", types: [Base(UI("E", []))] })]), Auto(8), Return([Var(Auto(8), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::minimal_filter::my_mod::ravencheck_tests::check_properties' (33) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb303856 - ravencheck::macro_examples::minimal_filter::my_mod::ravencheck_tests::check_properties::h4d49455eeee6ce68 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/minimal_filter.rs:1:1 [INFO] [stdout] 25: 0x5d4feb3038a7 - ravencheck::macro_examples::minimal_filter::my_mod::ravencheck_tests::check_properties::{{closure}}::h6b2b8abb672ac036 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/minimal_filter.rs:1:30 [INFO] [stdout] 26: 0x5d4feb310086 - core::ops::function::FnOnce::call_once::hd0292ffa41daaf3c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::type_parameter_sets::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [InstRule { left: UI("HashSet", [Base(UI("E", []))]), right: [Base(UI("E", []))] }] [INFO] [stdout] Pushing axiom with rules [InstRule { left: UI("HashSet", [Base(UI("E", []))]), right: [Base(UI("E", []))] }] [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Manual("s"), Base(UI("HashSet", [Base(UI("u32", []))])))], Bind1(Eq(false, [Var(Manual("s"), [])], [OpCode(ZeroArgAsConst, OpCode { ident: "empty_poly", types: [Base(UI("u32", []))] })]), Auto(31), Bind1(LogQuantifier(Forall, [(Manual("e"), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member_poly", types: [Base(UI("u32", []))] }, false), [Var(Manual("e"), []), Var(Manual("s"), [])]), Auto(35), Return([Var(Auto(35), [])]))), Auto(32), Bind1(LogOpN(And, [Var(Auto(31), []), Var(Auto(32), [])]), Auto(30), Return([Var(Auto(30), [])]))))), Auto(27), Return([Var(Auto(27), [])])) [INFO] [stdout] Did not match HashSet with u32 [INFO] [stdout] Matching HashSet with HashSet [INFO] [stdout] Subbing types [Base(UI("u32", []))] for ["E"] [INFO] [stdout] Inst axiom body: Bind1(LogQuantifier(Forall, [(Manual("e"), Base(UI("u32", [])))], BindN(Seq(BindN(Seq(Apply(BindN(Seq(Return([Var(Manual("empty_poly"), [Base(UI("u32", []))])])), [Atom(Auto(1))], Force(Var(Auto(1), []))), [], [])), [Atom(Auto(3))], BindN(Seq(Return([Var(Manual("e"), [])])), [Atom(Auto(2))], Apply(BindN(Seq(Return([Var(Manual("member_poly"), [Base(UI("u32", []))])])), [Atom(Auto(4))], Force(Var(Auto(4), []))), [], [Var(Auto(2), []), Var(Auto(3), [])])))), [Atom(Auto(5))], Bind1(LogNot(Var(Auto(5), [])), Auto(6), Return([Var(Auto(6), [])])))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] Did not match HashSet with u32 [INFO] [stdout] Matching HashSet with HashSet [INFO] [stdout] Subbing types [Base(UI("u32", []))] for ["E"] [INFO] [stdout] Inst axiom body: Bind1(LogQuantifier(Forall, [(Manual("s1"), Base(UI("HashSet", [Base(UI("u32", []))]))), (Manual("s2"), Base(UI("HashSet", [Base(UI("u32", []))])))], BindN(Seq(BindN(Seq(Return([Var(Manual("s1"), [])])), [Atom(Auto(11))], BindN(Seq(Return([Var(Manual("s2"), [])])), [Atom(Auto(12))], Bind1(Eq(true, [Var(Auto(11), [])], [Var(Auto(12), [])]), Auto(13), Return([Var(Auto(13), [])]))))), [Atom(Auto(15))], BindN(Seq(Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("u32", [])))], BindN(Seq(BindN(Seq(Return([Var(Manual("s1"), [])])), [Atom(Auto(3))], BindN(Seq(Return([Var(Manual("e"), [])])), [Atom(Auto(2))], Apply(BindN(Seq(Return([Var(Manual("member_poly"), [Base(UI("u32", []))])])), [Atom(Auto(4))], Force(Var(Auto(4), []))), [], [Var(Auto(2), []), Var(Auto(3), [])])))), [Atom(Auto(5))], BindN(Seq(BindN(Seq(Return([Var(Manual("s2"), [])])), [Atom(Auto(7))], BindN(Seq(Return([Var(Manual("e"), [])])), [Atom(Auto(6))], Apply(BindN(Seq(Return([Var(Manual("member_poly"), [Base(UI("u32", []))])])), [Atom(Auto(8))], Force(Var(Auto(8), []))), [], [Var(Auto(6), []), Var(Auto(7), [])])))), [Atom(Auto(9))], Bind1(Eq(false, [Var(Auto(5), [])], [Var(Auto(9), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Return([Var(Auto(1), [])]))), [Atom(Auto(14))], Bind1(LogOpN(Or, [Var(Auto(14), []), Var(Auto(15), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("e"), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member_poly", types: [Base(UI("u32", []))] }, false), [Var(Manual("e"), []), OpCode(ZeroArgAsConst, OpCode { ident: "empty_poly", types: [Base(UI("u32", []))] })]), Auto(8), Return([Var(Auto(8), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("s1"), Base(UI("HashSet", [Base(UI("u32", []))]))), (Manual("s2"), Base(UI("HashSet", [Base(UI("u32", []))])))], Bind1(Eq(true, [Var(Manual("s1"), [])], [Var(Manual("s2"), [])]), Auto(13), Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member_poly", types: [Base(UI("u32", []))] }, true), [Var(Manual("e"), []), Var(Manual("s1"), [])]), Auto(17), Bind1(LogOpN(Pred(OpCode { ident: "member_poly", types: [Base(UI("u32", []))] }, true), [Var(Manual("e"), []), Var(Manual("s2"), [])]), Auto(18), Bind1(Eq(false, [Var(Auto(17), [])], [Var(Auto(18), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Bind1(LogOpN(Or, [Var(Auto(1), []), Var(Auto(13), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::type_parameter_sets::my_mod::ravencheck_tests::check_properties' (45) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb2faefd - ravencheck::macro_examples::type_parameter_sets::my_mod::ravencheck_tests::check_properties::h018741bf1bf904fc [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/type_parameter_sets.rs:1:1 [INFO] [stdout] 25: 0x5d4feb2faf47 - ravencheck::macro_examples::type_parameter_sets::my_mod::ravencheck_tests::check_properties::{{closure}}::he305109d017d09a8 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/type_parameter_sets.rs:1:30 [INFO] [stdout] 26: 0x5d4feb30f0e6 - core::ops::function::FnOnce::call_once::h5f8edb9f0b0a8a5f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::sets_using_alias::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [] [INFO] [stdout] Pushing axiom with rules [] [INFO] [stdout] Expanding call union... [INFO] [stdout] Expanding call union... [INFO] [stdout] Expanding call union... [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Manual("a"), Base(UI("MySet", []))), (Manual("b"), Base(UI("MySet", [])))], Bind1(LogQuantifier(Exists, [(Auto(13), Base(UI("MySet", [])))], Bind1(LogOpN(Pred(OpCode { ident: "union", types: [] }, true), [Var(Manual("a"), []), Var(Manual("b"), []), Var(Auto(13), [])]), Auto(172), Bind1(LogQuantifier(Forall, [(Auto(16), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(16), []), Var(Auto(13), [])]), Auto(53), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(16), []), Var(Manual("a"), [])]), Auto(54), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(16), []), Var(Manual("b"), [])]), Auto(55), Bind1(LogOpN(Or, [Var(Auto(55), []), Var(Auto(54), [])]), Auto(29), Bind1(Eq(true, [Var(Auto(53), [])], [Var(Auto(29), [])]), Auto(181), Return([Var(Auto(181), [])]))))))), Auto(171), Bind1(LogQuantifier(Exists, [(Auto(14), Base(UI("MySet", [])))], Bind1(LogOpN(Pred(OpCode { ident: "union", types: [] }, true), [Var(Auto(13), []), Var(Manual("b"), []), Var(Auto(14), [])]), Auto(169), Bind1(LogQuantifier(Forall, [(Auto(61), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(61), []), Var(Auto(14), [])]), Auto(98), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(61), []), Var(Auto(13), [])]), Auto(99), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(61), []), Var(Manual("b"), [])]), Auto(100), Bind1(LogOpN(Or, [Var(Auto(100), []), Var(Auto(99), [])]), Auto(74), Bind1(Eq(true, [Var(Auto(98), [])], [Var(Auto(74), [])]), Auto(178), Return([Var(Auto(178), [])]))))))), Auto(168), Bind1(LogQuantifier(Exists, [(Auto(15), Base(UI("MySet", [])))], Bind1(LogOpN(Pred(OpCode { ident: "union", types: [] }, true), [Var(Manual("a"), []), Var(Manual("b"), []), Var(Auto(15), [])]), Auto(166), Bind1(LogQuantifier(Forall, [(Auto(106), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(106), []), Var(Auto(15), [])]), Auto(143), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(106), []), Var(Manual("a"), [])]), Auto(144), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Auto(106), []), Var(Manual("b"), [])]), Auto(145), Bind1(LogOpN(Or, [Var(Auto(145), []), Var(Auto(144), [])]), Auto(119), Bind1(Eq(true, [Var(Auto(143), [])], [Var(Auto(119), [])]), Auto(175), Return([Var(Auto(175), [])]))))))), Auto(165), Bind1(Eq(false, [Var(Auto(14), [])], [Var(Auto(15), [])]), Auto(170), Bind1(LogOpN(And, [Var(Auto(170), []), Var(Auto(171), []), Var(Auto(172), [])]), Auto(167), Bind1(LogOpN(And, [Var(Auto(167), []), Var(Auto(168), []), Var(Auto(169), [])]), Auto(164), Bind1(LogOpN(And, [Var(Auto(164), []), Var(Auto(165), []), Var(Auto(166), [])]), Auto(163), Return([Var(Auto(163), [])])))))))), Auto(160), Return([Var(Auto(160), [])]))))), Auto(157), Return([Var(Auto(157), [])]))))), Auto(154), Return([Var(Auto(154), [])]))), Auto(151), Return([Var(Auto(151), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("MySet", []))), (Manual("b"), Base(UI("MySet", [])))], Bind1(Eq(true, [Var(Manual("a"), [])], [Var(Manual("b"), [])]), Auto(13), Bind1(LogQuantifier(Exists, [(Manual("e"), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("a"), [])]), Auto(17), Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, true), [Var(Manual("e"), []), Var(Manual("b"), [])]), Auto(18), Bind1(Eq(false, [Var(Auto(17), [])], [Var(Auto(18), [])]), Auto(10), Return([Var(Auto(10), [])]))))), Auto(1), Bind1(LogOpN(Or, [Var(Auto(1), []), Var(Auto(13), [])]), Auto(16), Return([Var(Auto(16), [])]))))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("e"), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "member", types: [] }, false), [Var(Manual("e"), []), OpCode(ZeroArgAsConst, OpCode { ident: "empty_set", types: [] })]), Auto(8), Return([Var(Auto(8), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::sets_using_alias::my_mod::ravencheck_tests::check_properties' (44) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb2facc8 - ravencheck::macro_examples::sets_using_alias::my_mod::ravencheck_tests::check_properties::hc95a643de953e490 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/sets_using_alias.rs:12:1 [INFO] [stdout] 25: 0x5d4feb2fad17 - ravencheck::macro_examples::sets_using_alias::my_mod::ravencheck_tests::check_properties::{{closure}}::h06630f7187d83033 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/sets_using_alias.rs:12:30 [INFO] [stdout] 26: 0x5d4feb30fbd6 - core::ops::function::FnOnce::call_once::he22d86261bc82db0 [INFO] [stderr] error: test failed, to rerun pass `--lib` [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::import_test::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [InstRule { left: UI("Nat", [Base(UI("T", []))]), right: [Base(UI("T", []))] }] [INFO] [stdout] Pushing axiom with rules [InstRule { left: UI("Nat", [Base(UI("T", []))]), right: [Base(UI("T", []))] }] [INFO] [stdout] Expanding call dec::... [INFO] [stdout] Expanding call add::... [INFO] [stdout] Expanding call inc::... [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Auto(12), Base(UI("Nat", [Base(UI("T", []))]))), (Auto(13), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(Eq(true, [Var(Auto(12), [])], [OpCode(ZeroArgAsConst, OpCode { ident: "zero", types: [Base(UI("T", []))] })]), Auto(3), Ite(Var(Auto(3), []), Return([Literal(LogFalse)]), Bind1(LogQuantifier(Exists, [(Auto(19), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "dec", types: [Base(UI("T", []))] }, true), [Var(Auto(12), []), Var(Auto(19), [])]), Auto(139), Bind1(LogQuantifier(Exists, [(Auto(20), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "add", types: [Base(UI("T", []))] }, true), [Var(Auto(19), []), Var(Auto(13), []), Var(Auto(20), [])]), Auto(138), Bind1(Eq(true, [Var(Auto(13), [])], [Var(Auto(20), [])]), Auto(144), Bind1(Eq(false, [Var(Auto(19), [])], [OpCode(ZeroArgAsConst, OpCode { ident: "zero", types: [Base(UI("T", []))] })]), Auto(145), Bind1(LogOpN(Or, [Var(Auto(144), []), Var(Auto(145), [])]), Auto(141), Bind1(Eq(true, [Var(Auto(19), [])], [Var(Auto(20), [])]), Auto(142), Bind1(Eq(false, [Var(Auto(13), [])], [OpCode(ZeroArgAsConst, OpCode { ident: "zero", types: [Base(UI("T", []))] })]), Auto(143), Bind1(LogOpN(Or, [Var(Auto(142), []), Var(Auto(143), [])]), Auto(140), Bind1(LogOpN(And, [Var(Auto(140), []), Var(Auto(141), [])]), Auto(137), Bind1(LogQuantifier(Exists, [(Auto(21), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "inc", types: [Base(UI("T", []))] }, true), [Var(Auto(20), []), Var(Auto(21), [])]), Auto(135), Bind1(LogOpN(And, [Literal(LogFalse), Var(Auto(139), [])]), Auto(136), Bind1(LogOpN(And, [Var(Auto(136), []), Var(Auto(137), []), Literal(LogTrue), Var(Auto(138), [])]), Auto(134), Bind1(LogOpN(And, [Var(Auto(134), []), Var(Auto(135), [])]), Auto(133), Return([Var(Auto(133), [])])))))), Auto(130), Return([Var(Auto(130), [])]))))))))))), Auto(127), Return([Var(Auto(127), [])])))), Auto(124), Return([Var(Auto(124), [])]))))), Auto(121), Return([Var(Auto(121), [])])) [INFO] [stdout] Matching Nat with Nat [INFO] [stdout] Subbing types [Base(UI("T", []))] for ["T"] [INFO] [stdout] Inst axiom body: Bind1(LogQuantifier(Forall, [(Manual("x"), Base(UI("Nat", [Base(UI("T", []))])))], BindN(Seq(Return([Var(Manual("x"), [])])), [Atom(Auto(2))], BindN(Seq(Return([Var(Manual("x"), [])])), [Atom(Auto(1))], Apply(BindN(Seq(Return([Var(Manual("le"), [Base(UI("T", []))])])), [Atom(Auto(3))], Force(Var(Auto(3), []))), [], [Var(Auto(1), []), Var(Auto(2), [])])))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] Matching Nat with Nat [INFO] [stdout] Subbing types [Base(UI("T", []))] for ["T"] [INFO] [stdout] Inst axiom body: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("Nat", [Base(UI("T", []))])))], BindN(Seq(BindN(Seq(BindN(Seq(BindN(Seq(Return([Var(Manual("a"), [])])), [Atom(Auto(5))], Apply(BindN(Seq(Return([Var(Manual("dec"), [Base(UI("T", []))])])), [Atom(Auto(6))], Force(Var(Auto(6), []))), [], [Var(Auto(5), [])]))), [Atom(Auto(7))], Apply(BindN(Seq(Return([Var(Manual("inc"), [Base(UI("T", []))])])), [Atom(Auto(8))], Force(Var(Auto(8), []))), [], [Var(Auto(7), [])]))), [Atom(Auto(9))], BindN(Seq(Return([Var(Manual("a"), [])])), [Atom(Auto(10))], Bind1(Eq(true, [Var(Auto(9), [])], [Var(Auto(10), [])]), Auto(11), Return([Var(Auto(11), [])]))))), [Atom(Auto(13))], BindN(Seq(BindN(Seq(Return([Var(Manual("a"), [])])), [Atom(Auto(1))], BindN(Seq(Apply(BindN(Seq(Return([Var(Manual("zero"), [Base(UI("T", []))])])), [Atom(Auto(2))], Force(Var(Auto(2), []))), [], [])), [Atom(Auto(3))], Bind1(Eq(false, [Var(Auto(1), [])], [Var(Auto(3), [])]), Auto(4), Return([Var(Auto(4), [])]))))), [Atom(Auto(12))], Apply(BindN(Seq(Return([Var(Manual("implies"), [])])), [Atom(Auto(14))], Force(Var(Auto(14), []))), [], [Var(Auto(12), []), Var(Auto(13), [])])))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] Expanding call dec::... [INFO] [stdout] Expanding call inc::... [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("x"), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "le", types: [Base(UI("T", []))] }, true), [Var(Manual("x"), []), Var(Manual("x"), [])]), Auto(4), Return([Var(Auto(4), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogQuantifier(Forall, [(Auto(15), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "dec", types: [Base(UI("T", []))] }, false), [Var(Manual("a"), []), Var(Auto(15), [])]), Auto(37), Bind1(LogQuantifier(Forall, [(Auto(16), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "inc", types: [Base(UI("T", []))] }, false), [Var(Auto(15), []), Var(Auto(16), [])]), Auto(49), Bind1(Eq(true, [Var(Auto(16), [])], [Var(Manual("a"), [])]), Auto(11), Bind1(Eq(true, [Var(Manual("a"), [])], [OpCode(ZeroArgAsConst, OpCode { ident: "zero", types: [Base(UI("T", []))] })]), Auto(25), Bind1(LogOpN(Or, [Var(Auto(11), []), Var(Auto(25), [])]), Auto(21), Bind1(LogOpN(Or, [Var(Auto(21), []), Var(Auto(37), [])]), Auto(34), Bind1(LogOpN(Or, [Var(Auto(34), []), Var(Auto(49), [])]), Auto(46), Return([Var(Auto(46), [])])))))))), Auto(47), Return([Var(Auto(47), [])])))), Auto(35), Return([Var(Auto(35), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::import_test::my_mod::ravencheck_tests::check_properties' (27) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb30aca2 - ravencheck::macro_examples::import_test::my_mod::ravencheck_tests::check_properties::h7a3f16b12e784ae2 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/import_test.rs:1:1 [INFO] [stdout] 25: 0x5d4feb30acf7 - ravencheck::macro_examples::import_test::my_mod::ravencheck_tests::check_properties::{{closure}}::hf51fcef96afb209d [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/import_test.rs:1:30 [INFO] [stdout] 26: 0x5d4feb30f756 - core::ops::function::FnOnce::call_once::h1722d0b48a0fa29a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::nat::my_nat_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [InstRule { left: UI("Nat", [Base(UI("T", []))]), right: [Base(UI("T", []))] }] [INFO] [stdout] Pushing axiom with rules [InstRule { left: UI("Nat", [Base(UI("T", []))]), right: [Base(UI("T", []))] }] [INFO] [stdout] Expanding call dec::... [INFO] [stdout] Expanding call add::... [INFO] [stdout] Expanding call inc::... [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Auto(12), Base(UI("Nat", [Base(UI("T", []))]))), (Auto(13), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(Eq(true, [Var(Auto(12), [])], [OpCode(ZeroArgAsConst, OpCode { ident: "zero", types: [Base(UI("T", []))] })]), Auto(3), Ite(Var(Auto(3), []), Return([Literal(LogFalse)]), Bind1(LogQuantifier(Exists, [(Auto(19), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "dec", types: [Base(UI("T", []))] }, true), [Var(Auto(12), []), Var(Auto(19), [])]), Auto(139), Bind1(LogQuantifier(Exists, [(Auto(20), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "add", types: [Base(UI("T", []))] }, true), [Var(Auto(19), []), Var(Auto(13), []), Var(Auto(20), [])]), Auto(138), Bind1(Eq(true, [Var(Auto(13), [])], [Var(Auto(20), [])]), Auto(144), Bind1(Eq(false, [Var(Auto(19), [])], [OpCode(ZeroArgAsConst, OpCode { ident: "zero", types: [Base(UI("T", []))] })]), Auto(145), Bind1(LogOpN(Or, [Var(Auto(144), []), Var(Auto(145), [])]), Auto(141), Bind1(Eq(true, [Var(Auto(19), [])], [Var(Auto(20), [])]), Auto(142), Bind1(Eq(false, [Var(Auto(13), [])], [OpCode(ZeroArgAsConst, OpCode { ident: "zero", types: [Base(UI("T", []))] })]), Auto(143), Bind1(LogOpN(Or, [Var(Auto(142), []), Var(Auto(143), [])]), Auto(140), Bind1(LogOpN(And, [Var(Auto(140), []), Var(Auto(141), [])]), Auto(137), Bind1(LogQuantifier(Exists, [(Auto(21), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "inc", types: [Base(UI("T", []))] }, true), [Var(Auto(20), []), Var(Auto(21), [])]), Auto(135), Bind1(LogOpN(And, [Literal(LogFalse), Var(Auto(139), [])]), Auto(136), Bind1(LogOpN(And, [Var(Auto(136), []), Var(Auto(137), []), Literal(LogTrue), Var(Auto(138), [])]), Auto(134), Bind1(LogOpN(And, [Var(Auto(134), []), Var(Auto(135), [])]), Auto(133), Return([Var(Auto(133), [])])))))), Auto(130), Return([Var(Auto(130), [])]))))))))))), Auto(127), Return([Var(Auto(127), [])])))), Auto(124), Return([Var(Auto(124), [])]))))), Auto(121), Return([Var(Auto(121), [])])) [INFO] [stdout] Matching Nat with Nat [INFO] [stdout] Subbing types [Base(UI("T", []))] for ["T"] [INFO] [stdout] Inst axiom body: Bind1(LogQuantifier(Forall, [(Manual("x"), Base(UI("Nat", [Base(UI("T", []))])))], BindN(Seq(Return([Var(Manual("x"), [])])), [Atom(Auto(2))], BindN(Seq(Return([Var(Manual("x"), [])])), [Atom(Auto(1))], Apply(BindN(Seq(Return([Var(Manual("le"), [Base(UI("T", []))])])), [Atom(Auto(3))], Force(Var(Auto(3), []))), [], [Var(Auto(1), []), Var(Auto(2), [])])))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] Matching Nat with Nat [INFO] [stdout] Subbing types [Base(UI("T", []))] for ["T"] [INFO] [stdout] Inst axiom body: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("Nat", [Base(UI("T", []))])))], BindN(Seq(BindN(Seq(BindN(Seq(BindN(Seq(Return([Var(Manual("a"), [])])), [Atom(Auto(5))], Apply(BindN(Seq(Return([Var(Manual("dec"), [Base(UI("T", []))])])), [Atom(Auto(6))], Force(Var(Auto(6), []))), [], [Var(Auto(5), [])]))), [Atom(Auto(7))], Apply(BindN(Seq(Return([Var(Manual("inc"), [Base(UI("T", []))])])), [Atom(Auto(8))], Force(Var(Auto(8), []))), [], [Var(Auto(7), [])]))), [Atom(Auto(9))], BindN(Seq(Return([Var(Manual("a"), [])])), [Atom(Auto(10))], Bind1(Eq(true, [Var(Auto(9), [])], [Var(Auto(10), [])]), Auto(11), Return([Var(Auto(11), [])]))))), [Atom(Auto(13))], BindN(Seq(BindN(Seq(Return([Var(Manual("a"), [])])), [Atom(Auto(1))], BindN(Seq(Apply(BindN(Seq(Return([Var(Manual("zero"), [Base(UI("T", []))])])), [Atom(Auto(2))], Force(Var(Auto(2), []))), [], [])), [Atom(Auto(3))], Bind1(Eq(false, [Var(Auto(1), [])], [Var(Auto(3), [])]), Auto(4), Return([Var(Auto(4), [])]))))), [Atom(Auto(12))], Apply(BindN(Seq(Return([Var(Manual("implies"), [])])), [Atom(Auto(14))], Force(Var(Auto(14), []))), [], [Var(Auto(12), []), Var(Auto(13), [])])))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] Expanding call dec::... [INFO] [stdout] Expanding call inc::... [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("x"), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "le", types: [Base(UI("T", []))] }, true), [Var(Manual("x"), []), Var(Manual("x"), [])]), Auto(4), Return([Var(Auto(4), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogQuantifier(Forall, [(Auto(15), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "dec", types: [Base(UI("T", []))] }, false), [Var(Manual("a"), []), Var(Auto(15), [])]), Auto(37), Bind1(LogQuantifier(Forall, [(Auto(16), Base(UI("Nat", [Base(UI("T", []))])))], Bind1(LogOpN(Pred(OpCode { ident: "inc", types: [Base(UI("T", []))] }, false), [Var(Auto(15), []), Var(Auto(16), [])]), Auto(49), Bind1(Eq(true, [Var(Auto(16), [])], [Var(Manual("a"), [])]), Auto(11), Bind1(Eq(true, [Var(Manual("a"), [])], [OpCode(ZeroArgAsConst, OpCode { ident: "zero", types: [Base(UI("T", []))] })]), Auto(25), Bind1(LogOpN(Or, [Var(Auto(11), []), Var(Auto(25), [])]), Auto(21), Bind1(LogOpN(Or, [Var(Auto(21), []), Var(Auto(37), [])]), Auto(34), Bind1(LogOpN(Or, [Var(Auto(34), []), Var(Auto(49), [])]), Auto(46), Return([Var(Auto(46), [])])))))))), Auto(47), Return([Var(Auto(47), [])])))), Auto(35), Return([Var(Auto(35), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::nat::my_nat_mod::ravencheck_tests::check_properties' (35) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb30a50d - ravencheck::macro_examples::nat::my_nat_mod::ravencheck_tests::check_properties::h5080616ec876a1cd [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/nat.rs:1:1 [INFO] [stdout] 25: 0x5d4feb30a557 - ravencheck::macro_examples::nat::my_nat_mod::ravencheck_tests::check_properties::{{closure}}::h4dc21de454f28ef0 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/nat.rs:1:31 [INFO] [stdout] 26: 0x5d4feb30fad6 - core::ops::function::FnOnce::call_once::h0f7f9b9a67f4b805 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::main_example_nat::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [] [INFO] [stdout] Expanding call dec... [INFO] [stdout] Expanding call add... [INFO] [stdout] Expanding call inc... [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Auto(21), Base(UI("u32", []))), (Auto(22), Base(UI("u32", [])))], Bind1(Eq(true, [Var(Auto(21), [])], [Var(Manual("ZERO"), [])]), Auto(2), Bind1(Eq(true, [Var(Auto(21), [])], [Var(Manual("ZERO"), [])]), Auto(161), Ite(Var(Auto(2), []), Bind1(Eq(false, [Var(Auto(22), [])], [Var(Auto(22), [])]), Auto(162), Bind1(Eq(true, [Var(Auto(21), [])], [Var(Manual("ZERO"), [])]), Auto(163), Bind1(LogOpN(And, [Var(Auto(162), []), Var(Auto(163), [])]), Auto(159), Bind1(Eq(false, [Var(Auto(21), [])], [Var(Auto(22), [])]), Auto(160), Bind1(Eq(true, [Var(Auto(22), [])], [Var(Manual("ZERO"), [])]), Auto(2), Bind1(Eq(true, [Var(Auto(22), [])], [Var(Manual("ZERO"), [])]), Auto(161), Bind1(LogOpN(And, [Var(Auto(160), []), Var(Auto(161), [])]), Auto(158), Bind1(LogOpN(Or, [Var(Auto(158), []), Var(Auto(159), [])]), Auto(157), Return([Var(Auto(157), [])]))))))))), Bind1(LogQuantifier(Exists, [(Auto(44), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "dec", types: [] }, true), [Var(Auto(21), []), Var(Auto(44), [])]), Auto(179), Bind1(LogQuantifier(Exists, [(Auto(45), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "add", types: [] }, true), [Var(Auto(44), []), Var(Auto(22), []), Var(Auto(45), [])]), Auto(178), Bind1(Eq(true, [Var(Auto(22), [])], [Var(Auto(45), [])]), Auto(186), Bind1(Eq(false, [Var(Auto(44), [])], [Var(Manual("ZERO"), [])]), Auto(187), Bind1(LogOpN(Or, [Var(Auto(186), []), Var(Auto(187), [])]), Auto(183), Bind1(Eq(true, [Var(Auto(44), [])], [Var(Auto(45), [])]), Auto(184), Bind1(Eq(false, [Var(Auto(22), [])], [Var(Manual("ZERO"), [])]), Auto(185), Bind1(LogOpN(Or, [Var(Auto(184), []), Var(Auto(185), [])]), Auto(182), Bind1(LogOpN(And, [Var(Auto(182), []), Var(Auto(183), [])]), Auto(177), Bind1(LogQuantifier(Exists, [(Auto(46), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "inc", types: [] }, true), [Var(Auto(45), []), Var(Auto(46), [])]), Auto(175), Bind1(Eq(false, [Var(Auto(22), [])], [Var(Auto(46), [])]), Auto(162), Bind1(Eq(true, [Var(Auto(21), [])], [Var(Manual("ZERO"), [])]), Auto(163), Bind1(LogOpN(And, [Var(Auto(162), []), Var(Auto(163), [])]), Auto(181), Bind1(Eq(false, [Var(Auto(21), [])], [Var(Auto(46), [])]), Auto(160), Bind1(Eq(true, [Var(Auto(22), [])], [Var(Manual("ZERO"), [])]), Auto(161), Bind1(LogOpN(And, [Var(Auto(160), []), Var(Auto(161), [])]), Auto(180), Bind1(LogOpN(Or, [Var(Auto(180), []), Var(Auto(181), [])]), Auto(157), Bind1(LogOpN(And, [Var(Auto(157), []), Var(Auto(179), [])]), Auto(176), Bind1(LogOpN(And, [Var(Auto(176), []), Var(Auto(177), []), Var(Auto(178), [])]), Auto(174), Bind1(LogOpN(And, [Var(Auto(174), []), Var(Auto(175), [])]), Auto(173), Return([Var(Auto(173), [])]))))))))))))), Auto(170), Return([Var(Auto(170), [])]))))))))))), Auto(167), Return([Var(Auto(167), [])])))), Auto(164), Return([Var(Auto(164), [])])))))), Auto(154), Return([Var(Auto(154), [])])) [INFO] [stdout] Expanding call dec... [INFO] [stdout] Expanding call inc... [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("u32", [])))], Bind1(LogQuantifier(Forall, [(Auto(14), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "dec", types: [] }, false), [Var(Manual("a"), []), Var(Auto(14), [])]), Auto(36), Bind1(LogQuantifier(Forall, [(Auto(15), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "inc", types: [] }, false), [Var(Auto(14), []), Var(Auto(15), [])]), Auto(48), Bind1(Eq(true, [Var(Auto(15), [])], [Var(Manual("a"), [])]), Auto(10), Bind1(Eq(true, [Var(Manual("a"), [])], [Var(Manual("ZERO"), [])]), Auto(24), Bind1(LogOpN(Or, [Var(Auto(10), []), Var(Auto(24), [])]), Auto(20), Bind1(LogOpN(Or, [Var(Auto(20), []), Var(Auto(36), [])]), Auto(33), Bind1(LogOpN(Or, [Var(Auto(33), []), Var(Auto(48), [])]), Auto(45), Return([Var(Auto(45), [])])))))))), Auto(46), Return([Var(Auto(46), [])])))), Auto(34), Return([Var(Auto(34), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::main_example_nat::my_mod::ravencheck_tests::check_properties' (28) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb3065e0 - ravencheck::macro_examples::main_example_nat::my_mod::ravencheck_tests::check_properties::he7eb64831b71127b [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/main_example_nat.rs:1:1 [INFO] [stdout] 25: 0x5d4feb306637 - ravencheck::macro_examples::main_example_nat::my_mod::ravencheck_tests::check_properties::{{closure}}::h9c0dcaf6a6ba1b3e [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/main_example_nat.rs:1:30 [INFO] [stdout] 26: 0x5d4feb30f8a6 - core::ops::function::FnOnce::call_once::h42b395e83882c2cb [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] ---- macro_examples::nat_u32::my_mod::ravencheck_tests::check_properties stdout ---- [INFO] [stdout] Pushing axiom with rules [] [INFO] [stdout] Expanding call dec... [INFO] [stdout] Expanding call add... [INFO] [stdout] Expanding call inc... [INFO] [stdout] Checking 1 cases... [INFO] [stdout] Calling relevant_with_axioms on... [INFO] [stdout] term: Bind1(LogQuantifier(Exists, [(Auto(21), Base(UI("u32", []))), (Auto(22), Base(UI("u32", [])))], Bind1(Eq(true, [Var(Auto(21), [])], [Var(Manual("ZERO"), [])]), Auto(2), Bind1(Eq(true, [Var(Auto(21), [])], [Var(Manual("ZERO"), [])]), Auto(161), Ite(Var(Auto(2), []), Bind1(Eq(false, [Var(Auto(22), [])], [Var(Auto(22), [])]), Auto(162), Bind1(Eq(true, [Var(Auto(21), [])], [Var(Manual("ZERO"), [])]), Auto(163), Bind1(LogOpN(And, [Var(Auto(162), []), Var(Auto(163), [])]), Auto(159), Bind1(Eq(false, [Var(Auto(21), [])], [Var(Auto(22), [])]), Auto(160), Bind1(Eq(true, [Var(Auto(22), [])], [Var(Manual("ZERO"), [])]), Auto(2), Bind1(Eq(true, [Var(Auto(22), [])], [Var(Manual("ZERO"), [])]), Auto(161), Bind1(LogOpN(And, [Var(Auto(160), []), Var(Auto(161), [])]), Auto(158), Bind1(LogOpN(Or, [Var(Auto(158), []), Var(Auto(159), [])]), Auto(157), Return([Var(Auto(157), [])]))))))))), Bind1(LogQuantifier(Exists, [(Auto(44), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "dec", types: [] }, true), [Var(Auto(21), []), Var(Auto(44), [])]), Auto(179), Bind1(LogQuantifier(Exists, [(Auto(45), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "add", types: [] }, true), [Var(Auto(44), []), Var(Auto(22), []), Var(Auto(45), [])]), Auto(178), Bind1(Eq(true, [Var(Auto(22), [])], [Var(Auto(45), [])]), Auto(186), Bind1(Eq(false, [Var(Auto(44), [])], [Var(Manual("ZERO"), [])]), Auto(187), Bind1(LogOpN(Or, [Var(Auto(186), []), Var(Auto(187), [])]), Auto(183), Bind1(Eq(true, [Var(Auto(44), [])], [Var(Auto(45), [])]), Auto(184), Bind1(Eq(false, [Var(Auto(22), [])], [Var(Manual("ZERO"), [])]), Auto(185), Bind1(LogOpN(Or, [Var(Auto(184), []), Var(Auto(185), [])]), Auto(182), Bind1(LogOpN(And, [Var(Auto(182), []), Var(Auto(183), [])]), Auto(177), Bind1(LogQuantifier(Exists, [(Auto(46), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "inc", types: [] }, true), [Var(Auto(45), []), Var(Auto(46), [])]), Auto(175), Bind1(Eq(false, [Var(Auto(22), [])], [Var(Auto(46), [])]), Auto(162), Bind1(Eq(true, [Var(Auto(21), [])], [Var(Manual("ZERO"), [])]), Auto(163), Bind1(LogOpN(And, [Var(Auto(162), []), Var(Auto(163), [])]), Auto(181), Bind1(Eq(false, [Var(Auto(21), [])], [Var(Auto(46), [])]), Auto(160), Bind1(Eq(true, [Var(Auto(22), [])], [Var(Manual("ZERO"), [])]), Auto(161), Bind1(LogOpN(And, [Var(Auto(160), []), Var(Auto(161), [])]), Auto(180), Bind1(LogOpN(Or, [Var(Auto(180), []), Var(Auto(181), [])]), Auto(157), Bind1(LogOpN(And, [Var(Auto(157), []), Var(Auto(179), [])]), Auto(176), Bind1(LogOpN(And, [Var(Auto(176), []), Var(Auto(177), []), Var(Auto(178), [])]), Auto(174), Bind1(LogOpN(And, [Var(Auto(174), []), Var(Auto(175), [])]), Auto(173), Return([Var(Auto(173), [])]))))))))))))), Auto(170), Return([Var(Auto(170), [])]))))))))))), Auto(167), Return([Var(Auto(167), [])])))), Auto(164), Return([Var(Auto(164), [])])))))), Auto(154), Return([Var(Auto(154), [])])) [INFO] [stdout] Expanding call dec... [INFO] [stdout] Expanding call inc... [INFO] [stdout] axiom: Bind1(LogQuantifier(Forall, [(Manual("a"), Base(UI("u32", [])))], Bind1(LogQuantifier(Forall, [(Auto(14), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "dec", types: [] }, false), [Var(Manual("a"), []), Var(Auto(14), [])]), Auto(36), Bind1(LogQuantifier(Forall, [(Auto(15), Base(UI("u32", [])))], Bind1(LogOpN(Pred(OpCode { ident: "inc", types: [] }, false), [Var(Auto(14), []), Var(Auto(15), [])]), Auto(48), Bind1(Eq(true, [Var(Auto(15), [])], [Var(Manual("a"), [])]), Auto(10), Bind1(Eq(true, [Var(Manual("a"), [])], [Var(Manual("ZERO"), [])]), Auto(24), Bind1(LogOpN(Or, [Var(Auto(10), []), Var(Auto(24), [])]), Auto(20), Bind1(LogOpN(Or, [Var(Auto(20), []), Var(Auto(36), [])]), Auto(33), Bind1(LogOpN(Or, [Var(Auto(33), []), Var(Auto(48), [])]), Auto(45), Return([Var(Auto(45), [])])))))))), Auto(46), Return([Var(Auto(46), [])])))), Auto(34), Return([Var(Auto(34), [])]))), Auto(0), Return([Var(Auto(0), [])])) [INFO] [stdout] [INFO] [stdout] thread 'macro_examples::nat_u32::my_mod::ravencheck_tests::check_properties' (36) panicked at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69: [INFO] [stdout] called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: "No such file or directory" } [INFO] [stdout] stack backtrace: [INFO] [stdout] 0: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::libunwind::trace::hc4a5f428cfb78751 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:117:9 [INFO] [stdout] 1: 0x5d4feb5fd832 - std::backtrace_rs::backtrace::trace_unsynchronized::h20e1095684b4c296 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:14 [INFO] [stdout] 2: 0x5d4feb5fd832 - std::sys::backtrace::_print_fmt::h461f2e3a8f6b29e2 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:66:9 [INFO] [stdout] 3: 0x5d4feb5fd832 - ::fmt::h4ee3a75aa71a2c45 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:39:26 [INFO] [stdout] 4: 0x5d4feb62088f - core::fmt::rt::Argument::fmt::h6f1564705cd089af [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/rt.rs:173:76 [INFO] [stdout] 5: 0x5d4feb62088f - core::fmt::write::h21ca93b65a7c281a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/fmt/mod.rs:1468:25 [INFO] [stdout] 6: 0x5d4feb5ea4f3 - std::io::default_write_fmt::h6f3360f4711e9130 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:639:11 [INFO] [stdout] 7: 0x5d4feb5ea4f3 - std::io::Write::write_fmt::hf4539125c0e0bc30 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/io/mod.rs:1954:13 [INFO] [stdout] 8: 0x5d4feb5fde42 - std::sys::backtrace::BacktraceLock::print::h58d5d73f9e953cf1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:42:9 [INFO] [stdout] 9: 0x5d4feb5e89bc - std::panicking::default_hook::{{closure}}::h1457fbe47c9457d1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:301:27 [INFO] [stdout] 10: 0x5d4feb5e882e - std::panicking::default_hook::hccb5e73b206c0830 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:325:9 [INFO] [stdout] 11: 0x5d4feb31eeae - as core::ops::function::Fn>::call::h04940a86aa899793 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 12: 0x5d4feb31eeae - test::test_main_with_exit_callback::{{closure}}::hca6cc295403b83e8 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:145:21 [INFO] [stdout] 13: 0x5d4feb5e9743 - as core::ops::function::Fn>::call::h9d85285925beb538 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1985:9 [INFO] [stdout] 14: 0x5d4feb5e9743 - std::panicking::panic_with_hook::h3190ecc6229cdd29 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:842:13 [INFO] [stdout] 15: 0x5d4feb5fdc4a - std::panicking::panic_handler::{{closure}}::ha1f1b769bc2bb40c [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:707:13 [INFO] [stdout] 16: 0x5d4feb5fdba9 - std::sys::backtrace::__rust_end_short_backtrace::h5f9cf66f19c2a172 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:174:18 [INFO] [stdout] 17: 0x5d4feb5e93ed - __rustc[a93bd50104b99ad4]::rust_begin_unwind [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:698:5 [INFO] [stdout] 18: 0x5d4feb627b40 - core::panicking::panic_fmt::hc70c3c83f13c1375 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panicking.rs:75:14 [INFO] [stdout] 19: 0x5d4feb628e76 - core::result::unwrap_failed::ha809bf80017a514a [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1852:5 [INFO] [stdout] 20: 0x5d4feb42088b - core::result::Result::unwrap::h8b7a3df20a5ccfa5 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/result.rs:1223:23 [INFO] [stdout] 21: 0x5d4feb42088b - ravenlang::smt::query_negative_c::ha7455e0bc10a0a5d [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:464:69 [INFO] [stdout] 22: 0x5d4feb41ebec - ravenlang::smt::CheckedSig::check_goal::h5e3b1d37b0e98837 [INFO] [stdout] at /opt/rustwide/cargo-home/registry/src/index.crates.io-1949cf8c6b5b557f/ravenlang-0.3.0/src/smt/mod.rs:28:15 [INFO] [stdout] 23: 0x5d4feb2fb6ef - ravencheck::rcc::Rcc::check_goals::h476ef30fc5f613cf [INFO] [stdout] at /opt/rustwide/workdir/src/rcc.rs:316:23 [INFO] [stdout] 24: 0x5d4feb3104e0 - ravencheck::macro_examples::nat_u32::my_mod::ravencheck_tests::check_properties::h148e24962bc1263b [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/nat_u32.rs:1:1 [INFO] [stdout] 25: 0x5d4feb310537 - ravencheck::macro_examples::nat_u32::my_mod::ravencheck_tests::check_properties::{{closure}}::h7b63c60bb7b746f5 [INFO] [stdout] at /opt/rustwide/workdir/src/macro_examples/nat_u32.rs:1:30 [INFO] [stdout] 26: 0x5d4feb30f1a6 - core::ops::function::FnOnce::call_once::h8bd69eb84d06deea [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 27: 0x5d4feb31ff2b - core::ops::function::FnOnce::call_once::h70d190c46966003b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 28: 0x5d4feb31ff2b - test::__rust_begin_short_backtrace::hb077ccaabb17d2ec [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:663:18 [INFO] [stdout] 29: 0x5d4feb31db95 - test::run_test_in_process::{{closure}}::hd73eeb633a1507bd [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:74 [INFO] [stdout] 30: 0x5d4feb31db95 - as core::ops::function::FnOnce<()>>::call_once::h033c82756fc9d192 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 31: 0x5d4feb31db95 - std::panicking::catch_unwind::do_call::h734b44e243d34585 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 32: 0x5d4feb31db95 - std::panicking::catch_unwind::h5e85417122517fb1 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 33: 0x5d4feb31db95 - std::panic::catch_unwind::h0900e58a82a7d188 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 34: 0x5d4feb31db95 - test::run_test_in_process::h27721efd62ae77d0 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:686:27 [INFO] [stdout] 35: 0x5d4feb31db95 - test::run_test::{{closure}}::h8b1264838cc597aa [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:607:43 [INFO] [stdout] 36: 0x5d4feb344aa4 - test::run_test::{{closure}}::h6ecb96835e2eae4f [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/test/src/lib.rs:637:41 [INFO] [stdout] 37: 0x5d4feb344aa4 - std::sys::backtrace::__rust_begin_short_backtrace::h098f38ee82a820a7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/backtrace.rs:158:18 [INFO] [stdout] 38: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}::h042592f748f5e369 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:559:17 [INFO] [stdout] 39: 0x5d4feb32b6ba - as core::ops::function::FnOnce<()>>::call_once::h134fe7f3a2d9ec8d [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/panic/unwind_safe.rs:272:9 [INFO] [stdout] 40: 0x5d4feb32b6ba - std::panicking::catch_unwind::do_call::heb87d604f60aee16 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:590:40 [INFO] [stdout] 41: 0x5d4feb32b6ba - std::panicking::catch_unwind::h2203a0f553b89fd7 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panicking.rs:553:19 [INFO] [stdout] 42: 0x5d4feb32b6ba - std::panic::catch_unwind::h4d383e0b0e25d838 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/panic.rs:359:14 [INFO] [stdout] 43: 0x5d4feb32b6ba - std::thread::Builder::spawn_unchecked_::{{closure}}::h76cbdd4635cfd58b [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/thread/mod.rs:557:30 [INFO] [stdout] 44: 0x5d4feb32b6ba - core::ops::function::FnOnce::call_once{{vtable.shim}}::he72e066680f5e267 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/core/src/ops/function.rs:253:5 [INFO] [stdout] 45: 0x5d4feb5d3faf - as core::ops::function::FnOnce>::call_once::h1b9c6fea2cbefc68 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/alloc/src/boxed.rs:1971:9 [INFO] [stdout] 46: 0x5d4feb5d3faf - std::sys::pal::unix::thread::Thread::new::thread_start::h92caa992bc760789 [INFO] [stdout] at /rustc/b6ae10aa7319b7ebb6c7b3331dd71a9d6c9c5b4b/library/std/src/sys/pal/unix/thread.rs:107:17 [INFO] [stdout] 47: 0x77e3fda42aa4 - [INFO] [stdout] 48: 0x77e3fdacfa34 - clone [INFO] [stdout] 49: 0x0 - [INFO] [stdout] [INFO] [stdout] [INFO] [stdout] failures: [INFO] [stdout] macro_examples::filter::my_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::import_test::my_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::main_example_nat::my_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::main_example_set::my_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::minimal::my_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::minimal_filter::my_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::minimal_polymorphic::my_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::nat::my_nat_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::nat_u32::my_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::recursive::rvn::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::sets::my_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::sets_using_alias::my_mod::ravencheck_tests::check_properties [INFO] [stdout] macro_examples::type_parameter_sets::my_mod::ravencheck_tests::check_properties [INFO] [stdout] [INFO] [stdout] test result: FAILED. 7 passed; 13 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.29s [INFO] [stdout] [INFO] running `Command { std: "docker" "inspect" "a4824732bc49136f42d9736f8665808c96f09e90fd461193b135ffab4c4e6a75", kill_on_drop: false }` [INFO] running `Command { std: "docker" "rm" "-f" "a4824732bc49136f42d9736f8665808c96f09e90fd461193b135ffab4c4e6a75", kill_on_drop: false }` [INFO] [stdout] a4824732bc49136f42d9736f8665808c96f09e90fd461193b135ffab4c4e6a75