(set-logic QF_IDL)
(set-info :source |Example for Formal Techniques Summer School May 23, 2016 by
Clark Barrett
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const w Int)
(assert (<= (- x y) 5))
(assert (<= (- y x) (- 5)))
(assert (<= (- y z) (- 2)))
(assert (<= (- x z) (- 3)))
(assert (<= (- w x) 2))
(assert (<= (- x w) (- 2)))
(assert (<= (- z w) (- 1)))
(check-sat)