summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/strings-unconstrained.sy
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sygus/strings-unconstrained.sy')
-rw-r--r--test/regress/regress0/sygus/strings-unconstrained.sy8
1 files changed, 3 insertions, 5 deletions
diff --git a/test/regress/regress0/sygus/strings-unconstrained.sy b/test/regress/regress0/sygus/strings-unconstrained.sy
index 39c392487..49272165d 100644
--- a/test/regress/regress0/sygus/strings-unconstrained.sy
+++ b/test/regress/regress0/sygus/strings-unconstrained.sy
@@ -1,10 +1,9 @@
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
(synth-fun f ((firstname String) (lastname String)) String
-((Start String (ntString))
-
-(ntString String (
+((ntString String))
+((ntString String (
firstname
lastname
" "
@@ -12,4 +11,3 @@ lastname
))
(check-synth)
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback