blob: d96960c8316891407e812aeae43e99551ee2ac5a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
(synth-fun SC ((y (_ BitVec 32)) (w (_ BitVec 32)) ) (_ BitVec 32)
((Start (_ BitVec 32)) (StartBool Bool))
(
(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)
|