blob: d2a3700ce3ebb638e82bb46ba6715969aa0c1cd2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic ALL)
(synth-fun SC ((y (BitVec 32)) (w (BitVec 32)) ) (BitVec 32)
(
(Start (BitVec 32) (
y
w
#x00000000
(bvadd Start Start)
(ite StartBool Start Start)
))
(StartBool Bool ((= Start #x10000000) (= Start #x00000000)))
))
(constraint (= (SC #x00000000 #x00001000) #x00001000))
(constraint (= (SC #x00001000 #x00001000) #x00001000))
(constraint (= (SC #x01001000 #x00001000) #x01001000))
(check-synth)
|
