blob: 685718c3ec5894fdcf2e89aa9dec740f2c21b5ca (
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 a5)
(check-sat-assuming ( (not (or (or (or (or (or (or (or (or (or a0 a1) a2) a3) a4) a5) a6) a7) a8) a9)) ))
|
