diff options
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) |