Decision #953 — library/alloc/src/alloc.rs:128
Status: no_witness
Truth table
| row | c0 br 6190 | c1 br 6191 | outcome |
|---|---|---|---|
| 73523 | * | F | T |
| 73524 | * | F | T |
| 73525 | * | F | T |
| 73526 | * | F | T |
| 83406 | * | F | T |
| 83407 | * | F | T |
| 83408 | * | F | T |
| 83409 | * | F | T |
| 240109 | F | * | T |
| 240110 | F | * | T |
| 240111 | F | * | T |
| 240112 | F | * | T |
| 240113 | F | * | T |
| 240114 | F | * | T |
| 240115 | F | * | T |
| 240116 | F | * | T |
| 317486 | F | * | T |
| 317487 | F | * | T |
| 317488 | F | * | T |
| 317489 | F | * | T |
| 317490 | F | * | T |
| 317491 | F | * | T |
| 317492 | F | * | T |
| 317493 | F | * | T |
Independent-effect pairs
c0(branch6190): GAP view gap →<alloc::vec::Vec<scry_poly::Constraint> as alloc::vec::spec_from_iter_nested::SpecFromIterNested<scry_poly::Constraint, core::iter::adapters::cloned::Cloned<core::iter::adapters::filter::Filter<core::slice::iter::Iter<scry_poly::Constraint>, <scry_poly::Poly>::widen::{closure#0}>>>>::from_iter· br_ifc1(branch6191): GAP view gap →<alloc::vec::Vec<scry_poly::Constraint> as alloc::vec::spec_from_iter_nested::SpecFromIterNested<scry_poly::Constraint, core::iter::adapters::cloned::Cloned<core::iter::adapters::filter::Filter<core::slice::iter::Iter<scry_poly::Constraint>, <scry_poly::Poly>::widen::{closure#0}>>>>::from_iter· br_if