Function solve_sizes 

pub fn solve_sizes(
    conjuncts: &[Expr],
    arrays: &[ArrayState],
    var_tys: &[Ty],
    states: &[Option<BigUint>],
    blocked: &[Vec<usize>],
    seed: &mut u64,
) -> Result<SizeSolution, SizeError>

Chooses the sizes of the rand-active arrays whose size the size-eligible conjuncts constrain (module docs). var_tys[v] is the type of field variable v (conjuncts are over 0..var_tys.len()), states the state values, blocked size tuples ruled out by earlier attempts (in the sized order every call reproduces).