back-end that converts logical expressions to z3 and tests for their equivalence

A back-end that can compare spec1 (written by a student) and spec2 (written by the teaching) if they are equivalent. If they are not, then values that witness their inequivalence should also be produced.

added feature label

changed title from back-end that converts logical expressions to z3 and tests for their satisfiability to back-end that converts logical expressions to z3 and tests for their equivalence

closed

mentioned in issue #31 (closed)