From 0b283a384d4f276e2128c1eeb0817b7f8cf17636 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 21 Feb 2020 16:46:57 -0600 Subject: [PATCH] test: add some regression tests --- tests/sat/typed_v2l20091.cvc.smt2 | 31 ++++++++++++++++++++++++++ tests/sat/typed_v3l60005.cvc.smt2 | 34 +++++++++++++++++++++++++++++ tests/unsat/typed_v1l90014.cvc.smt2 | 28 ++++++++++++++++++++++++ 3 files changed, 93 insertions(+) create mode 100644 tests/sat/typed_v2l20091.cvc.smt2 create mode 100644 tests/sat/typed_v3l60005.cvc.smt2 create mode 100644 tests/unsat/typed_v1l90014.cvc.smt2 diff --git a/tests/sat/typed_v2l20091.cvc.smt2 b/tests/sat/typed_v2l20091.cvc.smt2 new file mode 100644 index 00000000..3828240c --- /dev/null +++ b/tests/sat/typed_v2l20091.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 sat) + + +(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 (= (ite ((_ is cons) x4) (cdr x4) null) null) (not (= (cons (leaf (ite ((_ is leaf) (leaf x2)) (data (leaf x2)) zero)) (cons x6 (ite ((_ is node) (leaf zero)) (children (leaf zero)) null))) null)))) +(check-sat) +(exit) + + diff --git a/tests/sat/typed_v3l60005.cvc.smt2 b/tests/sat/typed_v3l60005.cvc.smt2 new file mode 100644 index 00000000..901a07fb --- /dev/null +++ b/tests/sat/typed_v3l60005.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 sat) + + +(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 (not (= (leaf x3) (leaf (succ x1)))) (= x3 (ite ((_ is leaf) x8) (data x8) zero))) (not ((_ is cons) null))) (= x8 x9)) (= (node x5) (ite ((_ is cons) x6) (car x6) (leaf zero)))) (not (= x4 (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (cdr (ite ((_ is node) x9) (children x9) null)) null)) (cdr (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (cdr (ite ((_ is node) x9) (children x9) null)) null)) null)) (cdr (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (cdr (ite ((_ is node) x9) (children x9) null)) null)) (cdr (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (cdr (ite ((_ is node) x9) (children x9) null)) null)) null)) null))))) +(check-sat) +(exit) + + diff --git a/tests/unsat/typed_v1l90014.cvc.smt2 b/tests/unsat/typed_v1l90014.cvc.smt2 new file mode 100644 index 00000000..c82b6685 --- /dev/null +++ b/tests/unsat/typed_v1l90014.cvc.smt2 @@ -0,0 +1,28 @@ +(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 () list) +(declare-fun x3 () tree) + +(assert (and (and (and (and (and (and (and (and (not (= (cons (leaf x1) x2) (ite ((_ is cons) null) (cdr null) null))) (not (= (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is cons) (cons (leaf (succ (ite ((_ is leaf) (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) (data (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) zero))) (cons (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (car (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (leaf zero)) (ite ((_ is cons) (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) (cdr (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) null)))) (cdr (cons (leaf (succ (ite ((_ is leaf) (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) (data (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) zero))) (cons (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (car (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (leaf zero)) (ite ((_ is cons) (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) (cdr (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) null)))) null)) (cdr (ite ((_ is cons) (cons (leaf (succ (ite ((_ is leaf) (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) (data (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) zero))) (cons (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (car (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (leaf zero)) (ite ((_ is cons) (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) (cdr (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) null)))) (cdr (cons (leaf (succ (ite ((_ is leaf) (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) (data (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) zero))) (cons (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (car (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (leaf zero)) (ite ((_ is cons) (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) (cdr (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) null)))) null)) null)) (cdr (ite ((_ is cons) (ite ((_ is cons) (cons (leaf (succ (ite ((_ is leaf) (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) (data (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) zero))) (cons (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (car (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (leaf zero)) (ite ((_ is cons) (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) (cdr (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) null)))) (cdr (cons (leaf (succ (ite ((_ is leaf) (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) (data (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) zero))) (cons (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (car (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (leaf zero)) (ite ((_ is cons) (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) (cdr (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) null)))) null)) (cdr (ite ((_ is cons) (cons (leaf (succ (ite ((_ is leaf) (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) (data (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) zero))) (cons (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (car (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (leaf zero)) (ite ((_ is cons) (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) (cdr (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) null)))) (cdr (cons (leaf (succ (ite ((_ is leaf) (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) (data (ite ((_ is cons) (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (car (cons (leaf zero) (ite ((_ is cons) x2) (cdr x2) null))) (leaf zero))) zero))) (cons (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (car (ite ((_ is cons) (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) (cdr (ite ((_ is node) (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) (children (node (ite ((_ is cons) (ite ((_ is node) (node null)) (children (node null)) null)) (cdr (ite ((_ is node) (node null)) (children (node null)) null)) null))) null)) null)) (leaf zero)) (ite ((_ is cons) (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) (cdr (ite ((_ is node) (leaf (ite ((_ is succ) x1) (pred x1) zero))) (children (leaf (ite ((_ is succ) x1) (pred x1) zero))) null)) null)))) null)) null)) null) (ite ((_ is node) (leaf (succ (ite ((_ is succ) (ite ((_ is leaf) (leaf (ite ((_ is leaf) x3) (data x3) zero))) (data (leaf (ite ((_ is leaf) x3) (data x3) zero))) zero)) (pred (ite ((_ is leaf) (leaf (ite ((_ is leaf) x3) (data x3) zero))) (data (leaf (ite ((_ is leaf) x3) (data x3) zero))) zero)) zero)))) (children (leaf (succ (ite ((_ is succ) (ite ((_ is leaf) (leaf (ite ((_ is leaf) x3) (data x3) zero))) (data (leaf (ite ((_ is leaf) x3) (data x3) zero))) zero)) (pred (ite ((_ is leaf) (leaf (ite ((_ is leaf) x3) (data x3) zero))) (data (leaf (ite ((_ is leaf) x3) (data x3) zero))) zero)) zero)))) null)))) (= (node (ite ((_ is node) x3) (children x3) null)) (node (ite ((_ is cons) (ite ((_ is cons) null) (cdr null) null)) (cdr (ite ((_ is cons) null) (cdr null) null)) null)))) (not ((_ is node) (leaf (ite ((_ is leaf) x3) (data x3) zero))))) (not (= (ite ((_ is cons) (ite ((_ is node) x3) (children x3) null)) (cdr (ite ((_ is node) x3) (children x3) null)) null) null))) (not (= (cons (ite ((_ is cons) (ite ((_ is node) x3) (children x3) null)) (car (ite ((_ is node) x3) (children x3) null)) (leaf zero)) (ite ((_ is node) (leaf zero)) (children (leaf zero)) null)) (ite ((_ is node) (ite ((_ is cons) null) (car null) (leaf zero))) (children (ite ((_ is cons) null) (car null) (leaf zero))) null)))) (= (ite ((_ is succ) (ite ((_ is succ) zero) (pred zero) zero)) (pred (ite ((_ is succ) zero) (pred zero) zero)) zero) x1)) (not (= (ite ((_ is succ) (succ zero)) (pred (succ zero)) zero) (ite ((_ is leaf) (node null)) (data (node null)) zero)))) ((_ is null) null))) +(check-sat) +(exit) + +