diff options
Diffstat (limited to 'test/regress/regress1/sygus/phone-1-long.sy')
| -rw-r--r-- | test/regress/regress1/sygus/phone-1-long.sy | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/test/regress/regress1/sygus/phone-1-long.sy b/test/regress/regress1/sygus/phone-1-long.sy index 00a031ed4..0b402acf5 100644 --- a/test/regress/regress1/sygus/phone-1-long.sy +++ b/test/regress/regress1/sygus/phone-1-long.sy @@ -1,25 +1,21 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-fair=direct
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-fair=direct
; EXPECT: unsat
(set-logic SLIA)
-
+
(synth-fun f ((name String)) String
- ((Start String (ntString))
- (ntString String (name " "
+ ((ntString String) (ntInt Int))
+ ((ntString String (name " "
(str.++ ntString ntString)
(str.replace ntString ntString ntString)
(str.at ntString ntInt)
- (int.to.str ntInt)
+ (str.from_int ntInt)
(str.substr ntString ntInt ntInt)))
(ntInt Int (0 1 2 3 4 5
(+ ntInt ntInt)
(- ntInt ntInt)
(str.len ntString)
- (str.to.int ntString)
- (str.indexof ntString ntString ntInt)))
- (ntBool Bool (true false
- (str.prefixof ntString ntString)
- (str.suffixof ntString ntString)
- (str.contains ntString ntString)))))
+ (str.to_int ntString)
+ (str.indexof ntString ntString ntInt)))))
(declare-var name String)
(constraint (= (f "938-242-504") "242"))
|