source: vis_dev/cusp-1.1/examples/bignum_rdl2/bignum_rdl2.smt @ 31

Last change on this file since 31 was 12, checked in by cecile, 13 years ago

cusp added
File size: 562 bytes
Line 
1(benchmark bignum
2  :source { SMT-COMP'06 Organizers }
3  :notes "This benchmark is designed to check if the DP supports bignumbers."
4  :status unsat
5        :difficulty { 1 }
6        :category { check }
7  :logic QF_RDL
8  :extrafuns ((x1 Real))
9        :extrafuns ((x2 Real))
10        :extrafuns ((x3 Real))
11        :extrafuns ((x4 Real))
12  :formula
13  (and (< (- x1 x2) (/ 1 1000000000000000000000000000000000))
14                         (< (- x2 x3) (/ 1 2000000000000000000000000000000011))
15                         (< (- x3 x4) (~ (/ 1 1000000000000000000000000000000000)))
16                         (< (- x4 x1) (~ (/ 1 1999999999999999999999999999999988)))))
Note: See TracBrowser for help on using the repository browser.