pub fn symbolic<B: BV>(
ty: &Ty<Name>,
shared_state: &SharedState<'_, B>,
solver: &mut Solver<'_, B>,
) -> Result<Val<B>, ExecError>Expand description
Create a Symbolic value of a specified type. Can return a concrete value if the type only
permits a single value, such as for the unit type or the zero-length bitvector type (which is
ideal because SMT solvers don’t allow zero-length bitvectors). Compound types like structs will
be a concrete structure with symbolic values for each field. Returns the NoSymbolicType error
if the type cannot be represented in the SMT solver.