blob: 7d66908164e679ddfc113201253f559b876afa6d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic BV)
(synth-fun f (( x (_ BitVec 32))) (_ BitVec 32)
((BV32 (_ BitVec 32)) ( BV16 (_ BitVec 16)))
((BV32 (_ BitVec 32) (#x00000000 #x00000001 #xFFFFFFFF
x
(bvand BV32 BV32)
(bvor BV32 BV32)
(bvnot BV32)
(concat BV16 BV16)
))
(BV16 (_ BitVec 16) (#x0000 #x0001 #xFFFF
(bvand BV16 BV16)
(bvor BV16 BV16)
(bvnot BV16)
((_ extract 31 16) BV32)
((_ extract 15 0) BV32)))))
( constraint (= ( f #x0782ECAD ) #xECAD0000))
( constraint (= ( f #xFFFF008E ) #x008E0000))
( constraint (= ( f #x00000000 ) #x00000000))
( check-synth )
|
