mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
34 lines
1.2 KiB
Text
34 lines
1.2 KiB
Text
(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 (and (and (and (= x4 null) (not (= x5 (children x7)))) (not ((_ is leaf) (car null)))) (not ((_ is node) x8))) (= (data (leaf zero)) x3)) (not (= x9 x7))) (not (= (pred x2) (data x9)))) ((_ is null) (cdr x6))) (= (car null) (leaf (succ x1)))))
|
|
(check-sat)
|
|
(exit)
|
|
|
|
|