test/regress/regress1/quantifiers/bignum_quant.smt2


1
2
3
4
5
6
7
8
9
10
11
12

(set-logic AUFLIA)
(set-info :source | SMT-COMP'06 organizers |)
(set-info :smt-lib-version 2.0)
(set-info :category "check")
(set-info :status unsat)
(set-info :notes |This benchmark is designed to check if the DP supports bignumbers.|)
(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)