diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-30 14:11:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-30 14:11:16 -0500 |
commit | d36423fb74e3ec294b222b806cb24b5229e72ed1 (patch) | |
tree | c78260dd402be419cdc49e27f0cdb15ed14c7b08 /test/regress/regress1 | |
parent | 6538957335ecf83af38150054cf80555a57e72d0 (diff) |
Remove stoi solve rewrite (#2985)
Diffstat (limited to 'test/regress/regress1')
-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) |