diff options
Diffstat (limited to 'test/regress/regress1/strings')
| -rw-r--r-- | test/regress/regress1/strings/issue2981.smt2 | 20 | ||||
| -rw-r--r-- | test/regress/regress1/strings/stoi-solve.smt2 | 6 |
2 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/issue2981.smt2 b/test/regress/regress1/strings/issue2981.smt2 new file mode 100644 index 000000000..78cdb2a8c --- /dev/null +++ b/test/regress/regress1/strings/issue2981.smt2 @@ -0,0 +1,20 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status sat) +(declare-const x String) +(declare-const y String) +(declare-const m String) +(declare-const n String) +(assert (str.in.re x (re.+ (re.range "0" "9")))) +(assert (= 0 (str.to.int x))) +(assert (not (= x ""))) +(assert (not (= x "0"))) +(assert (not (= x "3"))) +(assert (not (= x "T"))) +(assert (not (= x "8"))) +(assert (not (= x ""))) +(assert (not (= x "5"))) +(assert (not (= x "<"))) +(assert (not (= x "N"))) +(check-sat) diff --git a/test/regress/regress1/strings/stoi-solve.smt2 b/test/regress/regress1/strings/stoi-solve.smt2 new file mode 100644 index 000000000..4fbbdcfc1 --- /dev/null +++ b/test/regress/regress1/strings/stoi-solve.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :strings-exp true) +(declare-fun x () String) +(assert (= (str.to.int x) 12345)) +(check-sat) |