diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-06 17:04:52 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-06 17:04:52 -0500 |
| commit | dd84403eb19b769d80b4c57ae690ba14c02df041 (patch) | |
| tree | aa63f0f909ecd7063e38f7121c17cafb431abdf4 /test | |
| parent | c87ee73ad3d51c238700f236c18e425b80e8e7ac (diff) | |
Minor clean up, fixes related to sygus.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/strings-unconstrained.sy | 15 |
2 files changed, 17 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 8c847be60..695c52cc6 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -49,7 +49,8 @@ TESTS = commutative.sy \ dt-test-ns.sy \ no-mention.sy \ max2-univ.sy \ - strings-small.sy + strings-small.sy \ + strings-unconstrained.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/strings-unconstrained.sy b/test/regress/regress0/sygus/strings-unconstrained.sy new file mode 100644 index 000000000..38e69e337 --- /dev/null +++ b/test/regress/regress0/sygus/strings-unconstrained.sy @@ -0,0 +1,15 @@ +; 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))) +)) + +(check-synth) + |