diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-20 18:31:27 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-20 18:31:27 -0600 |
commit | be91d86dd0f7b33f7c373c4d9bd40e207af910d2 (patch) | |
tree | a334962df5978aea72bbb2f5afcadf6eb0d29a99 /test/regress/regress0 | |
parent | 167b0386378346cadde0008b023a2c8ac143d2fd (diff) |
add more tests, and define int.to.str(NEGATIVE)=""
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/strings/type001.smt2 | 21 | ||||
-rw-r--r-- | test/regress/regress0/strings/type002.smt2 (renamed from test/regress/regress0/strings/int2str.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress0/strings/type003.smt2 (renamed from test/regress/regress0/strings/str2int.smt2) | 0 |
3 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2 new file mode 100644 index 000000000..ca93b00e5 --- /dev/null +++ b/test/regress/regress0/strings/type001.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun z () String)
+
+;big num test
+(assert (= x (int.to.str 4785582390527685649)))
+;should be ""
+(assert (= y (int.to.str (- 9))))
+
+;big num
+(assert (= i (str.to.int "783914785582390527685649")))
+;should be -1
+(assert (= j (str.to.int "-783914785582390527685649")))
+
+(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/int2str.smt2 b/test/regress/regress0/strings/type002.smt2 index ac4d9ab8a..ac4d9ab8a 100644 --- a/test/regress/regress0/strings/int2str.smt2 +++ b/test/regress/regress0/strings/type002.smt2 diff --git a/test/regress/regress0/strings/str2int.smt2 b/test/regress/regress0/strings/type003.smt2 index b8f0ac5ae..b8f0ac5ae 100644 --- a/test/regress/regress0/strings/str2int.smt2 +++ b/test/regress/regress0/strings/type003.smt2 |