blob: 2e6c6ef8108be63a1c16e613832386b32ec07596 (
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 --no-dump-synth
(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)
|