diff options
Diffstat (limited to 'test/regress/regress1/rr-verify/regex.sy')
| -rw-r--r-- | test/regress/regress1/rr-verify/regex.sy | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/test/regress/regress1/rr-verify/regex.sy b/test/regress/regress1/rr-verify/regex.sy index 6c6da3dd2..2d911e56a 100644 --- a/test/regress/regress1/rr-verify/regex.sy +++ b/test/regress/regress1/rr-verify/regex.sy @@ -1,17 +1,18 @@ -; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break ; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)' ; EXIT: 1 (set-logic SLIA) -(synth-fun f ((x String) (y String)) Bool ( +(synth-fun f ((x String) (y String)) Bool +((Start Bool) (StartRe RegLan) (StartStr String)) ( (Start Bool ( true false (= StartStr StartStr) - (str.in.re StartStr StartRe) + (str.in_re StartStr StartRe) )) (StartRe RegLan ( @@ -19,7 +20,7 @@ (re.++ StartRe StartRe) (re.union StartRe StartRe) (re.* StartRe) - (str.to.re StartStr) + (str.to_re StartStr) )) (StartStr String ( |