diff options
Diffstat (limited to 'test/regress/regress0/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy | 19 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/sygus-uf.sy | 4 |
2 files changed, 10 insertions, 13 deletions
diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy index 848ae0349..6a149cc71 100644 --- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy +++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy @@ -1,16 +1,16 @@ ; REQUIRES: no-competition ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 ; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type -; EXPECT-ERROR: +; EXPECT-ERROR: ; EXPECT-ERROR: (Op2 <O2> <F>) ; EXPECT-ERROR: ^ ; EXPECT-ERROR: ") ; EXIT: 1 -(set-logic ALL) +(set-logic HO_ALL) (set-option :lang sygus2) ;(set-option :sygus-out status) (set-option :sygus-rec-fun true) -(set-option :uf-ho true) + (define-sort Time () Int) @@ -47,19 +47,19 @@ (and (<= 0 t tn) (match f ( ((P i) (val t i)) - - ((Op1 op g) + + ((Op1 op g) (match op ( - (NOT (not (holds g t))) + (NOT (not (holds g t))) - (Y (and (< 0 t) (holds g (- t 1)))) + (Y (and (< 0 t) (holds g (- t 1)))) (G (and (holds g t) (or (= t tn) (holds f (+ t 1))))) (H (and (holds g t) (or (= t 0) (holds f (- t 1))))) ))) - ((Op2 op f g) + ((Op2 op f g) (match op ( (AND (and (holds f t) (holds g t))) @@ -88,6 +88,3 @@ (constraint (holds (Op1 G (phi X0 X1)) 0)) (check-synth) - - - diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy index b08aa8929..2f59598ec 100644 --- a/test/regress/regress0/sygus/sygus-uf.sy +++ b/test/regress/regress0/sygus/sygus-uf.sy @@ -1,6 +1,6 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho +; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-var uf (-> Int Int)) |