blob: ee011ceb4f9787a5611f169d6155d20e4df5f125 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(benchmark B_
:status unsat
:logic QF_BV
:extrafuns ((x0 BitVec[32]))
:extrafuns ((x1 BitVec[32]))
:extrafuns ((x2 BitVec[32]))
:extrafuns ((x3 BitVec[32]))
:extrafuns ((y0 BitVec[32]))
:extrafuns ((y1 BitVec[32]))
:extrafuns ((y2 BitVec[32]))
:extrafuns ((y3 BitVec[32]))
:assumption (= x0 x1)
:assumption (= x1 x2)
:assumption (= x2 x3)
:assumption (= y0 y1)
:assumption (= y1 y2)
:assumption (= y2 y3)
:assumption (= x0 y0)
:formula (not (= x3 y3))
)
|
