Negative coverage: `borrow_check_expr` / `binop` / premise `if scalar.is_int()`

Premise at line 487. Observed failure causes: if_false.

binop

Line	Coverage	Source
485	1	(borrow_check_expr(env, assumptions, state, lhs, rhs.live_before(env, &state, places_live_on_exit)) => (lhs_ty, state))
486	✗	(prove_ty_is_rigid(env, assumptions, state, &lhs_ty) => (RigidTy {name: RigidName::ScalarId(scalar), parameters: _}, state))
487	1	(if scalar.is_int())
488	3	(borrow_check_expr_has_ty(env, assumptions, state, rhs, &lhs_ty, places_live_on_exit) => state)
		──────── ("binop")
490	23	(borrow_check_expr(env, assumptions, state, Expr::BinOp{lhs, op: _, rhs}, places_live_on_exit) => (lhs_ty, state))

1 test failed proving this premise:

Source location: tests/mir_typeck.rs:1349 (all coverage from this test)

fn foo() -> () {
    let x: bool = true * false;
}

Failed proof tree

check_all_crates failed mod.rs:42
- args
- rule "check all prefixes" mod.rs:54
  - check_crate failed mod.rs:61
    
    args
    
    rule "check crate" mod.rs:74
    
    check_crate_item failed mod.rs:179
    
    rule "free fn" mod.rs:207
    
    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:54
    
    check_fn_body failed fns.rs:61
    
    args
    
    rule "expr fn body" fns.rs:89
    
    borrow_check failed nll.rs:124
    
    args
    
    rule "borrow_check" nll.rs:135
    
    borrow_check_block failed nll.rs:142
    
    rule "basic block" nll.rs:157
    
    borrow_check_statement failed nll.rs:174
    
    args
    
    rule "let" nll.rs:189
    
    borrow_check_expr_has_ty failed nll.rs:350
    
    args
    
    rule "block" nll.rs:363
    
    borrow_check_expr failed nll.rs:371
    
    args
    
    rule "multiplication" nll.rs:390
    
    borrow_check_expr failed nll.rs:371
    
    rule "binop" nll.rs:487 (failed: if_false)

How to read this page