Negative coverage: `prove_place_is_movable` / `field` / premise `if let None = env.program.find_drop_impl(adt_id)`

Premise at line 1001. Observed failure causes: if_let.

field

Line	Coverage	Source
1001	1	(if let None = env.program.find_drop_impl(adt_id))
1002	✗	(prove_place_is_movable(env, assumptions, state, prefix) => state)
		──────── ("field")
1004	3	(prove_place_is_movable( env, assumptions, state, TypedPlaceExpressionData::Field(prefix, _, adt_id, _), ) => state)

1 test failed proving this premise:

Source location: tests/borrowck.rs:3398

fn foo(f: Pair) -> () {
    let s: Datum = f.x;
}

Failed proof tree

check_all_crates failed mod.rs:41
- args
- rule "check all prefixes" mod.rs:53
  - check_crate failed mod.rs:60
    
    args
    
    rule "check crate" mod.rs:73
    
    check_crate_item failed mod.rs:178
    
    rule "free fn" mod.rs:206
    
    check_free_fn failed fns.rs:14
    
    args
    
    rule "check free fn" fns.rs:24
    
    check_fn failed fns.rs:31
    
    args
    
    rule "check fn" fns.rs:55
    
    check_fn_body failed fns.rs:62
    
    args
    
    rule "expr fn body" fns.rs:90
    
    borrow_check failed nll.rs:127
    
    args
    
    rule "borrow_check" nll.rs:138
    
    borrow_check_block failed nll.rs:145
    
    rule "basic block" nll.rs:160
    
    borrow_check_statement failed nll.rs:177
    
    args
    
    rule "let" nll.rs:194
    
    borrow_check_expr_has_ty failed nll.rs:351
    
    args
    
    rule "block" nll.rs:364
    
    borrow_check_expr failed nll.rs:372
    
    args
    
    rule "place" nll.rs:506
    
    prove_place_is_movable failed nll.rs:975
    
    args
    
    rule "field" nll.rs:1001 (failed: if_let)