source: vis_dev/cusp-1.1/examples/bignum_rdl1/bignum_rdl1.smt @ 43

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

cusp added
File size: 564 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 sat
5        :difficulty { 2 }
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 2000000000000000000000000000000012)))))
Note: See TracBrowser for help on using the repository browser.