blob: abcfc2217701320395fd30c8c659b662c52b4e25 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status
(set-logic BV)
(define-fun hd19 ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32)
(bvxor x (bvxor (bvshl (bvand (bvxor (bvlshr x k) x) m) k) (bvand (bvxor (bvlshr x k) x) m))))
; bvand is a duplicate
(synth-fun f ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32)
((Start (BitVec 32) ((bvand Start Start)
(bvsub Start Start)
(bvxor Start Start)
(bvor Start Start)
(bvand Start Start)
(bvshl Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvnot Start)
(bvneg Start)
x
m
k))))
(declare-var x (BitVec 32))
(declare-var m (BitVec 32))
(declare-var k (BitVec 32))
(constraint (= (hd19 x m k) (f x m k)))
(check-synth)
|
