blob: 9a28d6d7918b27ca4bab3387aad6a6b81d92effd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --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)))
((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)
|
