Pick two 8-bit formulas to compare
(assert (not (= f1 f2))) then (check-sat)