test/regress/regress1/sygus/max2-bv.sy


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

; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic BV)

(synth-fun max2 ((x (BitVec 32))(y (BitVec 32))) (BitVec 32)
)

(declare-var x (BitVec 32))

(declare-var y (BitVec 32))

(constraint 
(bvuge (max2 x y) x)
)

(constraint 
(bvuge (max2 x y) y)
)

(constraint 
(or (= x (max2 x y)) (= y (max2 x y)))
)

(check-synth)