tests

simple-cong.cnf

@@ -0,0 +1,24 @@
+p cnf 10 10
+1 0
+2 0
+3 0
+c 4 0
+-9 6 0
+c 5 0
+-8 -10 0
+6 -7 -8 0
+-6 8 0
+-6 7 0
+9 0
+10 -1 -2 0
+
+c 1 (= a b)
+c 2 (= c d)
+c 3 (and p1 true)
+c 4 (or (not p1) (and p2 p3))
+c 5 (or (not p3) (not (= (f a c) (f b d))))
+c 6 (and p2 p3)
+c 7 (not p2)
+c 8 (not p3)
+c 9 p1
+c 10 (= (f a c) (f b d))

simple-cong.smt2

@@ -0,0 +1,24 @@
+(set-logic QF_UF)
+(set-option :simplification none)
+
+(declare-sort U 0)
+
+(declare-const p1 Bool)
+(declare-const p2 Bool)
+(declare-const p3 Bool)
+
+(declare-const a U)
+(declare-const b U)
+(declare-const c U)
+(declare-const d U)
+(declare-fun f (U U) U)
+
+(assert (= a b))
+(assert (= c d))
+(assert (and p1 true))
+(assert (or (not p1) (and p2 p3)))
+(assert (or (not p3) (not (= (f a c) (f b d)))))
+
+; (or (not (= a b)) (not (= c d)) (= (f a c) (f b d)))
+
+(check-sat)