kdrag.utils.all_values

kdrag.utils.all_values(*es: ExprRef) → Generator[list[ExprRef], None, None]

Generate all values possible for an expression. Generator won’t terminate if there are infinite possible values. Concretization.

>>> assert set(all_values(smt.If(smt.Bool("x"), 2, 3))) == {smt.IntVal(2), smt.IntVal(3)}