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 | |
| parent | 6538957335ecf83af38150054cf80555a57e72d0 (diff) | |
Remove stoi solve rewrite (#2985)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue2981.smt2 | 20 | ||||
| -rw-r--r-- | test/regress/regress1/strings/stoi-solve.smt2 (renamed from test/regress/regress0/strings/stoi-solve.smt2) | 0 |
3 files changed, 22 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c9514dd76..d8adbb59e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -846,7 +846,6 @@ set(regress_0_tests regress0/strings/rewrites-re-concat.smt2 regress0/strings/rewrites-v2.smt2 regress0/strings/std2.6.1.smt2 - regress0/strings/stoi-solve.smt2 regress0/strings/str003.smt2 regress0/strings/str004.smt2 regress0/strings/str005.smt2 @@ -1537,6 +1536,7 @@ set(regress_1_tests regress1/strings/issue1684-regex.smt2 regress1/strings/issue2060.smt2 regress1/strings/issue2429-code.smt2 + regress1/strings/issue2981.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 @@ -1569,6 +1569,7 @@ set(regress_1_tests regress1/strings/replaceall-replace.smt2 regress1/strings/rew-020618.smt2 regress1/strings/stoi-400million.smt2 + regress1/strings/stoi-solve.smt2 regress1/strings/str-code-sat.smt2 regress1/strings/str-code-unsat-2.smt2 regress1/strings/str-code-unsat-3.smt2 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/regress0/strings/stoi-solve.smt2 b/test/regress/regress1/strings/stoi-solve.smt2 index 4fbbdcfc1..4fbbdcfc1 100644 --- a/test/regress/regress0/strings/stoi-solve.smt2 +++ b/test/regress/regress1/strings/stoi-solve.smt2 |