diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress0/sygus/strings-small.sy | |
parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress0/sygus/strings-small.sy')
-rw-r--r-- | test/regress/regress0/sygus/strings-small.sy | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy deleted file mode 100644 index 7d976ff39..000000000 --- a/test/regress/regress0/sygus/strings-small.sy +++ /dev/null @@ -1,35 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -(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) - |