diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-03 15:53:52 -0500 |
|---|---|---|
| committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-04-03 15:53:52 -0500 |
| commit | e1f463c0884dccf8fe513bd59bfd7ba6a8592183 (patch) | |
| tree | e695789b17bcff3ab2565cd701fc09a1fa21e322 /test/regress | |
| parent | 8a9ffdbb248ddcc6a41f628f6dcbc070b57e6a28 (diff) | |
Fix combination of datatypes + strings in PBE (#2930)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue2914.sy | 26 |
2 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 13d1540f6..a9b807e82 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1624,6 +1624,7 @@ set(regress_1_tests regress1/sygus/inv-example.sy regress1/sygus/inv-missed-sol-true.sy regress1/sygus/inv-unused.sy + regress1/sygus/issue2914.sy regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy diff --git a/test/regress/regress1/sygus/issue2914.sy b/test/regress/regress1/sygus/issue2914.sy new file mode 100644 index 000000000..0f125a870 --- /dev/null +++ b/test/regress/regress1/sygus/issue2914.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) +(declare-datatype JSIdentifier ((JSString (jsString String)) (Error ))) + +(synth-fun substring ((x1 String) (x3 Int))String + ((Start String (ntString)) + (ntInt Int + (0 x3) + ) + (ntJSIdentifier JSIdentifier + ( + Error + ) + ) + (ntString String + (x1 + (str.substr ntString ntInt ntInt) + (jsString ntJSIdentifier) + (str.++ ntString ntString) + ) + ) + ) +) +(constraint (= (substring "ey" 1) "e")) +(check-synth) |