diff options
Diffstat (limited to 'test/regress/regress0/sygus/strings-small.sy')
-rw-r--r-- | test/regress/regress0/sygus/strings-small.sy | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy new file mode 100644 index 000000000..40346bcdf --- /dev/null +++ b/test/regress/regress0/sygus/strings-small.sy @@ -0,0 +1,35 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth +(set-logic SLIA) +(synth-fun f ((firstname String) (lastname String)) String +((Start String (ntString)) + +(ntString String ( +firstname +lastname +" " +(str.++ ntString ntString))) + +(ntInt Int ( +0 +1 +2 +(+ ntInt ntInt) +(- ntInt ntInt) +(str.len ntString) +(str.to.int ntString) +(str.indexof ntString ntString ntInt))) + +(ntBool Bool ( +true +false +(str.prefixof ntString ntString) +(str.suffixof ntString ntString) +(str.contains ntString ntString))) + +)) + +(constraint (= (f "Nancy" "FreeHafer") "Nancy FreeHafer")) + +(check-synth) + |