src/lfsc/tests/lia1.smt2


1
2
3
4
5
6
7
8

(set-logic QF_LIA)

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (not (=> (and (<= x 3) (or (not (>= y 8)) (not (>= z 10)))) (or (not (>= (+ x y) 11)) (not (>= (+ x z) 13))))))
(check-sat)
(exit)