diff options
Diffstat (limited to 'test/regress/regress1/sygus/sygus-dt.sy')
| -rw-r--r-- | test/regress/regress1/sygus/sygus-dt.sy | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/test/regress/regress1/sygus/sygus-dt.sy b/test/regress/regress1/sygus/sygus-dt.sy index 336c59b27..7539fdd0d 100644 --- a/test/regress/regress1/sygus/sygus-dt.sy +++ b/test/regress/regress1/sygus/sygus-dt.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification (set-logic LIA) @@ -7,8 +7,10 @@ (define-fun g ((x Int)) List (cons (+ x 1) nil)) (define-fun i () List (cons 3 nil)) -(synth-fun f ((x Int)) List ((Start List ((g StartInt) i (cons StartInt Start) nil (tail Start))) - (StartInt Int (x 0 1 (+ StartInt StartInt))))) +(synth-fun f ((x Int)) List + ((Start List) (StartInt Int)) + ((Start List ((g StartInt) i (cons StartInt Start) nil (tail Start))) + (StartInt Int (x 0 1 (+ StartInt StartInt))))) (declare-var x Int) |