blob: fc715a645889382cc17331177df09dca69a1ae54 (
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: --sygus-out=status
(set-logic BV)
(define-sort BV () (_ BitVec 8))
(synth-fun IC ((s BV) (t BV)) Bool
((Start Bool (
true
false
(ite Start Start Start)
(= (bvmul StartBv s) t)
))
(StartBv BV (
s
t
#x00
#x01
#x7E
(bvnot StartBv)
(bvmul StartBv StartBv)
(bvudiv StartBv StartBv)
(bvurem StartBv StartBv)
(bvand StartBv StartBv)
))
))
(constraint (not (IC (_ bv32 8) (_ bv187 8) )))
(constraint (not (IC (_ bv102 8) (_ bv15 8) )))
(constraint (not (IC (_ bv92 8) (_ bv85 8) )))
(constraint (IC (_ bv39 8) (_ bv214 8) ))
(constraint (IC (_ bv155 8) (_ bv82 8) ))
(constraint (IC (_ bv53 8) (_ bv98 8) ))
(constraint (IC (_ bv41 8) (_ bv47 8) ))
(check-synth)
|
