diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-05 15:31:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-04-05 15:31:20 -0500 |
| commit | 880f0b719479ff9f9b415749b2ccf9016274a99d (patch) | |
| tree | 0dedb4e4d7cd427885a681259237b5ef3a8e2662 /test | |
| parent | afc70ac962185b97e10f4e796f46c638ed1e18ab (diff) | |
Fix another corner case of datatypes+PBE (#2938)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue2935.sy | 36 |
2 files changed, 37 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a9b807e82..64da9ec61 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1625,6 +1625,7 @@ set(regress_1_tests regress1/sygus/inv-missed-sol-true.sy regress1/sygus/inv-unused.sy regress1/sygus/issue2914.sy + regress1/sygus/issue2935.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/issue2935.sy b/test/regress/regress1/sygus/issue2935.sy new file mode 100644 index 000000000..5616d19f5 --- /dev/null +++ b/test/regress/regress1/sygus/issue2935.sy @@ -0,0 +1,36 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) +(declare-datatype JSIdentifier ((JSInt (jsInt Int)) (JSString (jsString String)) )) + +(synth-fun f ((x1_ JSIdentifier)(x2_ String)) JSIdentifier + ((Start JSIdentifier (ntJSIdentifier)) + (ntInt Int + (1 + (+ ntInt ntInt) + (jsInt ntJSIdentifier) + ) + ) + (ntString String + (x2_ + (str.substr ntString ntInt ntInt) + (jsString ntJSIdentifier) + ) + ) + (ntBool Bool + ( + (= ntString ntString) + ) + ) + (ntJSIdentifier JSIdentifier + ( x1_ + (ite ntBool ntJSIdentifier ntJSIdentifier) + (JSString ntString) + ) + ) + ) +) +(constraint (= (f (JSString "") "") (JSString ""))) +(constraint (= (f (JSString "M") "W") (JSString "M"))) +(constraint (= (f (JSString "Moon") "") (JSString "on"))) +(check-synth) |