more unsat tests

tests/unsat/eq_diamond17.smt2

@@ -0,0 +1,63 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UF)
+(set-info :source |
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. |)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun x0 () U)
+(declare-fun y0 () U)
+(declare-fun z0 () U)
+(declare-fun x1 () U)
+(declare-fun y1 () U)
+(declare-fun z1 () U)
+(declare-fun x2 () U)
+(declare-fun y2 () U)
+(declare-fun z2 () U)
+(declare-fun x3 () U)
+(declare-fun y3 () U)
+(declare-fun z3 () U)
+(declare-fun x4 () U)
+(declare-fun y4 () U)
+(declare-fun z4 () U)
+(declare-fun x5 () U)
+(declare-fun y5 () U)
+(declare-fun z5 () U)
+(declare-fun x6 () U)
+(declare-fun y6 () U)
+(declare-fun z6 () U)
+(declare-fun x7 () U)
+(declare-fun y7 () U)
+(declare-fun z7 () U)
+(declare-fun x8 () U)
+(declare-fun y8 () U)
+(declare-fun z8 () U)
+(declare-fun x9 () U)
+(declare-fun y9 () U)
+(declare-fun z9 () U)
+(declare-fun x10 () U)
+(declare-fun y10 () U)
+(declare-fun z10 () U)
+(declare-fun x11 () U)
+(declare-fun y11 () U)
+(declare-fun z11 () U)
+(declare-fun x12 () U)
+(declare-fun y12 () U)
+(declare-fun z12 () U)
+(declare-fun x13 () U)
+(declare-fun y13 () U)
+(declare-fun z13 () U)
+(declare-fun x14 () U)
+(declare-fun y14 () U)
+(declare-fun z14 () U)
+(declare-fun x15 () U)
+(declare-fun y15 () U)
+(declare-fun z15 () U)
+(declare-fun x16 () U)
+(assert (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) (or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) (or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) (or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) (or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) (or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) (or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) (or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) (or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) (or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) (or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) (or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) (or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) (or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15))) (or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16))) (not (= x0 x16))))
+(check-sat)
+(exit)

tests/unsat/typed_v2l20025.cvc.smt2

@@ -0,0 +1,31 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_DT)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2017-04-28
+Generator: Random, converted to v2.6 by CVC4
+Application: Regressions for datatypes decision procedure.
+Target solver: CVC3
+Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "random")
+(set-info :status unsat)
+
+
+(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))
+((cons (car tree) (cdr list)) (null))
+((node (children list)) (leaf (data nat)))
+))
+(declare-fun x1 () nat)
+(declare-fun x2 () nat)
+(declare-fun x3 () list)
+(declare-fun x4 () list)
+(declare-fun x5 () tree)
+(declare-fun x6 () tree)
+
+(assert (and ((_ is cons) x4) (= (cons (node x4) x3) (ite ((_ is cons) x4) (cdr x4) null))))
+(check-sat)
+(exit)
+
+

tests/unsat/typed_v3l60024.cvc.smt2

@@ -0,0 +1,34 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_DT)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2017-04-28
+Generator: Random, converted to v2.6 by CVC4
+Application: Regressions for datatypes decision procedure.
+Target solver: CVC3
+Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "random")
+(set-info :status unsat)
+
+
+(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))
+((cons (car tree) (cdr list)) (null))
+((node (children list)) (leaf (data nat)))
+))
+(declare-fun x1 () nat)
+(declare-fun x2 () nat)
+(declare-fun x3 () nat)
+(declare-fun x4 () list)
+(declare-fun x5 () list)
+(declare-fun x6 () list)
+(declare-fun x7 () tree)
+(declare-fun x8 () tree)
+(declare-fun x9 () tree)
+
+(assert (and (and (and (and (and (= (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (cdr (ite ((_ is node) x9) (children x9) null)) null) (cons x9 x6)) (= (ite ((_ is leaf) (node x6)) (data (node x6)) zero) (ite ((_ is leaf) (ite ((_ is cons) x5) (car x5) (leaf zero))) (data (ite ((_ is cons) x5) (car x5) (leaf zero))) zero))) (not ((_ is succ) zero))) (not (= x7 x8))) (not ((_ is leaf) x7))) (= (ite ((_ is cons) x6) (cdr x6) null) (ite ((_ is cons) null) (cdr null) null))))
+(check-sat)
+(exit)
+
+

tests/unsat/typed_v5l50010.cvc.smt2

@@ -0,0 +1,40 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_DT)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2017-04-28
+Generator: Random, converted to v2.6 by CVC4
+Application: Regressions for datatypes decision procedure.
+Target solver: CVC3
+Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "random")
+(set-info :status unsat)
+
+
+(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))
+((cons (car tree) (cdr list)) (null))
+((node (children list)) (leaf (data nat)))
+))
+(declare-fun x1 () nat)
+(declare-fun x2 () nat)
+(declare-fun x3 () nat)
+(declare-fun x4 () nat)
+(declare-fun x5 () nat)
+(declare-fun x6 () list)
+(declare-fun x7 () list)
+(declare-fun x8 () list)
+(declare-fun x9 () list)
+(declare-fun x10 () list)
+(declare-fun x11 () tree)
+(declare-fun x12 () tree)
+(declare-fun x13 () tree)
+(declare-fun x14 () tree)
+(declare-fun x15 () tree)
+
+(assert (and (and (and (and (= (succ x3) (ite ((_ is succ) x3) (pred x3) zero)) (not ((_ is node) x11))) (not ((_ is leaf) x13))) (not (= (ite ((_ is node) x12) (children x12) null) x6))) (= (ite ((_ is node) x14) (children x14) null) x8)))
+(check-sat)
+(exit)
+
+