diff options
Diffstat (limited to 'test/regress/regress1/sygus/fg_polynomial3.sy')
| -rw-r--r-- | test/regress/regress1/sygus/fg_polynomial3.sy | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/test/regress/regress1/sygus/fg_polynomial3.sy b/test/regress/regress1/sygus/fg_polynomial3.sy index d70516bf1..2da3809a8 100644 --- a/test/regress/regress1/sygus/fg_polynomial3.sy +++ b/test/regress/regress1/sygus/fg_polynomial3.sy @@ -1,13 +1,11 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) -(synth-fun addExpr1 ((x Int) (y Int)) Int -) +(synth-fun addExpr1 ((x Int) (y Int)) Int) -(synth-fun addExpr2 ((x Int) (y Int)) Int -) +(synth-fun addExpr2 ((x Int) (y Int)) Int) (declare-var x Int) (declare-var y Int) @@ -15,4 +13,3 @@ (constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x (+ x y)))) (check-synth) - |