blob: d8cf9cf99ce29ac8e0baa0b4daa78809f4b7bb66 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status sat)
(declare-fun v0 () (_ BitVec 16))
(declare-fun v1 () (_ BitVec 16))
(declare-fun v2 () (_ BitVec 16))
(declare-fun v3 () (_ BitVec 16))
(declare-fun v4 () (_ BitVec 16))
(declare-fun v5 () (_ BitVec 16))
(declare-fun v6 () (_ BitVec 16))
(declare-fun v7 () (_ BitVec 16))
(declare-fun v8 () (_ BitVec 16))
(declare-fun v9 () (_ BitVec 16))
(assert (and
(bvult v6 v5)
(bvule v7 v8)
(bvugt v7 v1)
(bvuge v4 v1)
(bvuge v8 v0)
(bvugt v1 v0)
(bvuge v1 (_ bv60094 16))
(bvule v3 v0)
(bvuge (_ bv47327 16) v6)
(bvugt v3 v6)
))
(check-sat)
(exit)
|
