diff options
Diffstat (limited to 'test/regress/regress1/sygus/issue2935.sy')
| -rw-r--r-- | test/regress/regress1/sygus/issue2935.sy | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/test/regress/regress1/sygus/issue2935.sy b/test/regress/regress1/sygus/issue2935.sy index 5616d19f5..ea8011a5e 100644 --- a/test/regress/regress1/sygus/issue2935.sy +++ b/test/regress/regress1/sygus/issue2935.sy @@ -1,10 +1,18 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) -(declare-datatype JSIdentifier ((JSInt (jsInt Int)) (JSString (jsString String)) )) + +(declare-datatype JSIdentifier ((JSInt (jsInt Int)) (JSString (jsString String)))) (synth-fun f ((x1_ JSIdentifier)(x2_ String)) JSIdentifier - ((Start JSIdentifier (ntJSIdentifier)) + ((ntJSIdentifier JSIdentifier) (ntInt Int) (ntString String) (ntBool Bool)) + ( + (ntJSIdentifier JSIdentifier + (x1_ + (ite ntBool ntJSIdentifier ntJSIdentifier) + (JSString ntString) + ) + ) (ntInt Int (1 (+ ntInt ntInt) @@ -18,19 +26,15 @@ ) ) (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) |