mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 09:40:21 +00:00
21 lines
812 B
Plaintext
21 lines
812 B
Plaintext
(set-logic AUFLIRA)
|
|
(set-info :source | Buggy list theorem |)
|
|
(set-info :smt-lib-version 2.0)
|
|
(set-info :category "crafted")
|
|
(set-info :status sat)
|
|
(declare-sort List 0)
|
|
(declare-fun cons (Real List) List)
|
|
(declare-fun nil () List)
|
|
(declare-fun car (List) Real)
|
|
(declare-fun cdr (List) List)
|
|
(declare-fun len (List) Int)
|
|
(assert (forall ((?x Real) (?y List)) (= (car (cons ?x ?y)) ?x)))
|
|
(assert (forall ((?x Real) (?y List)) (= (cdr (cons ?x ?y)) ?y)))
|
|
(assert (= (len nil) 0))
|
|
(assert (forall ((?x Real) (?y List)) (= (len (cons ?x ?y)) (+ (len ?y) 1))))
|
|
(declare-fun append (List List) List)
|
|
(assert (forall ((?x Real) (?y1 List) (?y2 List)) (= (append (cons ?x ?y1) ?y2) (cons ?x (append ?y1 ?y2)))))
|
|
(assert (not (forall ((?x Real) (?y List)) (= (append (cons ?x nil) ?y) (cons ?x ?y)))))
|
|
(check-sat)
|
|
(exit)
|