blob: b84e5bb4825a16117d8cc38083f7b04d605d1734 (
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
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --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)) (Const (_ 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)
|
