blob: d809e7e9a2e94e21313b940b2a99adfa76688c9e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(set-info :source | SMT-COMP'06 organizers |)
(set-info :smt-lib-version 2.0)
(set-info :category "check")
(set-info :status unsat)
(set-logic AUFLIA)
(set-info :notes |This benchmark is designed to check if the DP supports bignumbers.| )
(set-info :difficulty 0.000)
(declare-fun f (Int) Int)
(assert (= (f 0) 1))
(assert (forall (?x Int) (=> (> ?x 0) (= (f ?x) (* (- 1000) (f (- ?x 1)))))))
(assert (< (f 20) 0))
(check-sat)
(exit)
|
