Exercise 8 - ccExample.smt2
ccTest.smt2
—
Plain Text,
206 bytes
File contents
(set-logic QF_UF) (declare-sort U 0) (declare-fun a () U) (declare-fun b () U) (declare-fun f (U) U) (assert (= (f (f (f a))) a)) (assert (= (f (f (f (f (f a))))) a)) (assert (distinct (f a) a)) (check-sat)