Negative coverage: check_crate_item / adt / premise check_adt(program, &s.to_adt()) => ()

Premise at line 185. Observed failure causes: failed_judgment.

3 tests failed proving this premise:

Source location: tests/basic_tests.rs:277

#[test]
fn basic_adt_variant_dup() {
    FormalityTest::new(crates![crate Foo {
        enum Bar {
            Baz{},
            Baz{},
        }
    }])
    .err(expect_test::expect![[r#"
        the rule "check adt" at (adts.rs) failed because
          variant "Baz" defined multiple times"#]])
}

Source location: tests/basic_tests.rs:290

#[test]
fn basic_adt_field_dup() {
    FormalityTest::new(crates![crate Foo {
        struct Bar {
            baz: (),
            baz: (),
        }
    }])
    .err(expect_test::expect![[r#"
        the rule "check adt" at (adts.rs) failed because
          field "baz" of variant "struct" defined multiple times"#]])
}

Source location: tests/well_formed_trait_ref.rs:37

#[test]
fn missing_dependent_where_clause() {
    FormalityTest::new(crates![crate foo {
        trait Trait1 {}

        trait Trait2 {}

        struct S1<T> where T: Trait1 {
            dummy: T,
        }

        struct S2<T> where S1<T> : Trait2 {
            dummy: T,
        }
    }])
    .err(expect_test::expect![[r#"
        crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: @ WellFormedTraitRef(Trait2(S1<!ty_0>)), via: Trait2(S1<!ty_0>), assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: Trait1(!ty_0), via: Trait2(S1<!ty_0>), assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "trait implied bound" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.trait_invariants()`"#]])
}