blob: b54c7688b20002bcb1ea0f7658ca65c8de88225f (
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
33
34
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all
(set-logic BV)
(define-fun B ((h (BitVec 8)) (l (BitVec 8)) (v (BitVec 8))) (BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l))))
(define-fun E ((x (BitVec 8))) (BitVec 8) (bvadd x #x41))
(define-fun f ((x (BitVec 8))) (BitVec 8) (bvsub x #x41))
(define-fun d ((x (BitVec 8))) Bool (bvule x #x3f))
(synth-fun D ((x (BitVec 8)) (y (BitVec 8)) ) (BitVec 8)
((Start (BitVec 8) (
(f Start) x y Const
(bvshl Start Start) (bvnot Start)
(bvand Start Start)
(bvxor Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvlshr Start Start)
(bvsub Start Start)
))
(Const (BitVec 8) (#x01 #x03 #x06 #x07 #x04 #x05 #x02 #x00))
))
(declare-var x (BitVec 8))
(constraint (= x (D (E (B #x07 #x04 x) ) (E (B #x03 #x00 x)) )) )
; notice we don't have solution reconstruction for this
(check-synth)
|
