Function encodings_semantically_equal
pub fn encodings_semantically_equal<'ctx, A: Arch>(
options: &EncodingComparisonOptions,
a: &Encoding<A, SynthesizedComputation>,
b: &Encoding<A, SynthesizedComputation>,
solver: &mut impl SmtSolver<'ctx>,
) -> Equivalence
Expand description
Determines whether two encodings are semantically equivalent.
This function assumes both encodings describe the exact same instruction space.