1 files changed, 38 insertions, 0 deletions
diff --git a/test/regress/regress0/uf/cnf-iff.smt2 b/test/regress/regress0/uf/cnf-iff.smt2
new file mode 100644
index 000000000..03377005c
--- /dev/null
+++ b/test/regress/regress0/uf/cnf-iff.smt2
@@ -0,0 +1,38 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort U 0)
+
+(declare-fun f (U) U)
+(declare-fun g (U) U)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(declare-fun e () U)
+(declare-fun h () U)
+(declare-fun i () U)
+
+(assert (or 
+(= a c)
+(= h c)
+(not (= h d))
+(not (= h e))
+(= h i)
+(= (= (f a) d) (= d (f b)))
+(= (not (= (f a) d)) (not (= d (f b))))
+(not (= (not (= d (f b))) (= (f a) d)))
+(not (= (= d (f b)) (not (= (f a) d))))
+(xor (= (f a) d) (not (= d (f b))))
+(xor (not (= (f a) d)) (= d (f b)))
+(not (xor (= (f a) d) (= d (f b))))
+(not (xor (not (= (f a) d)) (not (= d (f b)))))
+))
+(assert (not (= h i)))
+(assert (or (not (= (f a) d)) (not (= d (f b)))))
+(assert (or (= (f a) d) (= d (f b))))
+(assert (and (not (= b e)) (not (= c a))))
+(assert (and (= h e) (not (= b e))))
+
+(assert (not (or (= b h) (= c h))))
+(assert (not (or (= b h) (not (= d h)))))
+(check-sat)