1 files changed, 168 insertions, 0 deletions
diff --git a/src/lfsc/tests/dead_dnd001_and.smt2 b/src/lfsc/tests/dead_dnd001_and.smt2
new file mode 100644
index 0000000..4d93b9e
--- /dev/null
+++ b/src/lfsc/tests/dead_dnd001_and.smt2
@@ -0,0 +1,168 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+
+(declare-sort I 0)
+(declare-fun f (I I) I)
+(declare-fun a () I)
+(declare-fun b () I)
+(declare-fun c () I)
+
+
+(assert
+(and
+ (or
+  (= (f a a) a)
+  (or (= (f a a) b)
+      (= (f a a) c))
+  )
+
+(and
+ (or
+  (= (f a b) a)
+  (or (= (f a b) b)
+      (= (f a b) c))
+  )
+
+(and
+ (or
+  (= (f a c) a)
+  (or (= (f a c) b)
+      (= (f a c) c))
+  )
+
+(and
+ (or
+  (= (f b a) a)
+  (or (= (f b a) b)
+      (= (f b a) c))
+  )
+
+(and
+ (or
+  (= (f b b) a)
+  (or (= (f b b) b)
+      (= (f b b) c))
+  )
+
+(and
+ (or
+  (= (f b c) a)
+  (or (= (f b c) b)
+      (= (f b c) c))
+  )
+
+
+(and
+ (or
+  (= (f c a) a)
+  (or (= (f c a) b)
+      (= (f c a) c))
+  )
+
+(and
+ (or
+  (= (f c b) a)
+  (or (= (f c b) b)
+      (= (f c b) c))
+  )
+
+(and
+ (or
+  (= (f c c) a)
+  (or (= (f c c) b)
+      (= (f c c) c))
+  )
+
+
+
+(and
+ (or
+  (= (f a a) a)
+  (or (= (f b b) a)
+      (= (f c c) a))
+  )
+
+(and
+ (or
+  (= (f a a) b)
+  (or (= (f b b) b)
+      (= (f c c) b))
+  )
+
+(and
+ (or
+  (= (f a a) c)
+  (or (= (f b b) c)
+      (= (f c c) c))
+  )
+
+
+
+(and
+ (or
+  (= (f a a) a)
+  (or (= (f b a) b)
+      (= (f c a) c))
+  )
+
+(and
+ (or
+  (= (f a b) a)
+  (or (= (f b b) b)
+      (= (f c b) c))
+  )
+
+(and
+ (or
+  (= (f a c) a)
+  (or (= (f b c) b)
+      (= (f c c) c))
+  )
+
+
+
+
+(and (not (= (f a a) a))
+(and (not (= (f b b) b))
+(and (not (= (f c c) c))
+
+
+(and
+ (or
+  (not (= (f a (f a a)) a))
+  (or (not (= (f a (f a b)) b))
+      (not (= (f a (f a c)) c)))
+  )
+
+(and
+ (or
+  (not (= (f b (f b a)) a)) 
+  (or (not (= (f b (f b b)) b))
+      (not (= (f b (f b c)) c)))
+  )
+
+(and
+ (or
+  (not (= (f c (f c a)) a)) 
+  (or (not (= (f c (f c b)) b))
+      (not (= (f c (f c c)) c)))
+  )
+
+
+(and  (not (= (f a a) (f b a)))
+(and  (not (= (f a a) (f c a)))
+(and  (not (= (f b a) (f c a)))
+
+(and  (not (= (f a b) (f b b)))
+(and  (not (= (f a b) (f c b)))
+(and  (not (= (f b b) (f c b)))
+
+(and  (not (= (f a c) (f b c)))
+(and  (not (= (f a c) (f c c)))
+  (not (= (f b c) (f c c))))
+
+)))))))))))))))))))))))))))))
+
+(check-sat)
+
+(exit)