unit-tests/ex1.smt2


1
2
3
4
5
6
7
8
9
10
11

(set-logic QF_SAT)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)

(assert (not (=> (and (=> a b) (=> b c)) (=> a c))))

(check-sat)

(exit)