diff options
Diffstat (limited to 'test/regress/regress1/sygus/issue2914.sy')
-rw-r--r-- | test/regress/regress1/sygus/issue2914.sy | 26 |
1 files changed, 26 insertions, 0 deletions
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) |