source: vis_dev/cusp-1.1/examples/bignum_idl1/bignum_idl1.smt @ 23

Last change on this file since 23 was 12, checked in by cecile, 14 years ago

cusp added
  • Property svn:executable set to *
File size: 538 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_IDL
8  :extrafuns ((x1 Int))
9        :extrafuns ((x2 Int))
10        :extrafuns ((x3 Int))
11        :extrafuns ((x4 Int))
12  :formula
13  (and (<= (- x1 x2) 1000000000000000000000000000000000)
14                         (<= (- x2 x3) 2000000000000000000000000000000011)
15                         (<= (- x3 x4) (~ 1000000000000000000000000000000000))
16                         (<= (- x4 x1) (~ 2000000000000000000000000000000012))))
Note: See TracBrowser for help on using the repository browser.