blob: 2bd8fc0dc8f7d29fbba0db85a9501764be14f7e8 (
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
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32)
((Start (_ BitVec 32)) (StartBool Bool))
((Start (_ BitVec 32)
(
(bvudiv Start Start)
(bvurem Start Start)
(bvsdiv Start Start)
#x00000001
#x00000000
#x00000002 x
(ite StartBool Start Start)))
(StartBool Bool (( bvult Start Start)
(bvugt Start Start)
(= Start Start)
))))
(declare-var x (_ BitVec 32) )
; property
(constraint (= (f #x00000008) #x00000004))
(constraint (= (f #x00000010) #x00000008))
(constraint (not (= (f x) #xffffffff)))
(check-synth)
|
