diff options
Diffstat (limited to 'test/regress/regress1/sygus/inv_gen_fig8.sy')
| -rw-r--r-- | test/regress/regress1/sygus/inv_gen_fig8.sy | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test/regress/regress1/sygus/inv_gen_fig8.sy b/test/regress/regress1/sygus/inv_gen_fig8.sy index 19c36e4dc..5c1aa4852 100644 --- a/test/regress/regress1/sygus/inv_gen_fig8.sy +++ b/test/regress/regress1/sygus/inv_gen_fig8.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun inv ((l Int)) Bool ( @@ -8,9 +8,9 @@ (AtomicFormula Bool ((<= Sum Const) (= Sum Const))) (Sum Int ((+ Term Term))) (Term Int ((* Sign Var))) - (Sign Int (0 1 -1)) + (Sign Int (0 1 (- 1))) (Var Int (l)) - (Const Int (-3 -2 -1 0 1 2 3)) + (Const Int ((- 3) (- 2) (- 1) 0 1 2 3)) ) ) @@ -36,11 +36,11 @@ (declare-var x4p Int) (constraint (implies (and6 (= l 0) (or (= x0p (+ x0 1)) (= x0p (- x0 1))) - (or (= x1p (+ x1 1)) (= x1p (- x1 1))) - (or (= x2p (+ x2 1)) (= x2p (- x2 1))) - (or (= x3p (+ x3 1)) (= x3p (- x3 1))) - (or (= x4p (+ x4 1)) (= x4p (- x4 1)))) - (inv l))) + (or (= x1p (+ x1 1)) (= x1p (- x1 1))) + (or (= x2p (+ x2 1)) (= x2p (- x2 1))) + (or (= x3p (+ x3 1)) (= x3p (- x3 1))) + (or (= x4p (+ x4 1)) (= x4p (- x4 1)))) + (inv l))) (constraint (implies (and (inv l) (not (= l 0))) false)) (check-synth) |