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

Determines whether two encodings are semantically equivalent.

This function assumes both encodings describe the exact same instruction space.