blob: d4bf1f3d40da04d36953b0f0c456f25145db1fe6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
; EXPECT: unsat
(set-logic ALL)
(set-option :incremental false)
(declare-fun a0 () Bool)
(declare-fun a1 () Bool)
(declare-fun a2 () Bool)
(declare-fun a3 () Bool)
(declare-fun a4 () Bool)
(declare-fun a5 () Bool)
(declare-fun a6 () Bool)
(declare-fun a7 () Bool)
(declare-fun a8 () Bool)
(declare-fun a9 () Bool)
(assert (not a5))
(check-sat-assuming ( (not (not (and (and (and (and (and (and (and (and (and a0 a1) a2) a3) a4) a5) a6) a7) a8) a9))) ))
|
