(ufbv) refutation unsoudness

[zhendongsu]

Commit: 54a8d65
OS: Ubuntu 18.04

[586] % z3release small.smt2
unsat
sat
[587] % cat small.smt2
(declare-sort S 0)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f () S)
(declare-fun f1 () S)
(declare-fun f2 (S1 S) S)
(declare-fun f3 (S2 S) S1)
(declare-fun f4 () S)
(declare-fun f5 () S2)
(assert (not (= f1 (f2 (f3 f5 f4) f))))
(assert (not (= f f4)))
(assert (forall ((q S) (v S)) (or (= q v) (= f1 (f2 (f3 f5 q) v)) (= (f2 (f3 f5 v) q) f1))))
(assert (forall ((q S)) (not (= (f2 (f3 f5 q) q) f1))))
(check-sat-using ufbv)
(check-sat)