blob: 1379d42063fb5e0a2f6cb3d3f106d12013fbaf56 (
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: --cegqi --sygus-out=status
(set-logic BV)
(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x (bvsub x #x00000001)))
(synth-fun f ((x (BitVec 32))) (BitVec 32)
((Start (BitVec 32) ((bvand Start Start)
(bvsub Start Start)
(bvor Start Start)
(bvadd Start Start)
(bvxor Start Start)
x
#x00000000
#xFFFFFFFF
#x00000001))))
(declare-var x (BitVec 32))
(constraint (= (hd01 x) (f x)))
(check-synth)
|
