diff options
Diffstat (limited to 'test/regress/regress1/sygus/max2-bv.sy')
| -rw-r--r-- | test/regress/regress1/sygus/max2-bv.sy | 23 |
1 files changed, 7 insertions, 16 deletions
diff --git a/test/regress/regress1/sygus/max2-bv.sy b/test/regress/regress1/sygus/max2-bv.sy index 297bd9179..fa98ef26b 100644 --- a/test/regress/regress1/sygus/max2-bv.sy +++ b/test/regress/regress1/sygus/max2-bv.sy @@ -1,26 +1,17 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) -(synth-fun max2 ((x (BitVec 32))(y (BitVec 32))) (BitVec 32) -) +(synth-fun max2 ((x (_ BitVec 32)) (y (_ BitVec 32))) (_ BitVec 32)) -(declare-var x (BitVec 32)) +(declare-var x (_ BitVec 32)) -(declare-var y (BitVec 32)) +(declare-var y (_ BitVec 32)) -(constraint -(bvuge (max2 x y) x) -) +(constraint (bvuge (max2 x y) x)) -(constraint -(bvuge (max2 x y) y) -) +(constraint (bvuge (max2 x y) y)) -(constraint -(or (= x (max2 x y)) (= y (max2 x y))) -) +(constraint (or (= x (max2 x y)) (= y (max2 x y)))) (check-synth) - - |