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


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-bv
(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)