source: vis_dev/cusp-1.1/examples/int_incompleteness1/int_incompleteness1.smt @ 20

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

cusp added
  • Property svn:executable set to *
File size: 390 bytes
Line 
1(benchmark int_incompleteness1.smt
2  :source { Leonardo de Moura }
3  :notes "This benchmark is designed to check if the integer DP is complete."
4  :status unsat
5  :difficulty { 0 }
6  :category { check }
7  :logic QF_IDL
8  :extrafuns ((x1 Int) (x2 Int))
9  :formula
10  (and (> (- x1 x2) 0)
11                         (< (- x1 x2) 4)
12                         (not (= (- x1 x2) 1))
13                         (not (= (- x1 x2) 2))
14                         (not (= (- x1 x2) 3))))
15
16
17
18
Note: See TracBrowser for help on using the repository browser.