diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-28 07:10:15 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-28 14:10:15 +0000 |
| commit | f4894f5e0630bd3610699b13a8abae3e0ce9e600 (patch) | |
| tree | 1fe02f3123d1c8e556530089764742081d3f541a | |
| parent | 972dcfafe5eeb10b7b45892d1291000e73746c76 (diff) | |
Disable `--jh-rlv-order` for slow regressions (#6633)
This commit adds --no-jh-rlv-order to two string regressions that take
over 2 minutes to run in debug after #6613, which increases the overall
regression runtime significantly.
| -rw-r--r-- | test/regress/regress1/strings/stoi-400million.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress2/strings/issue6057-replace-re-all.smt2 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress1/strings/stoi-400million.smt2 b/test/regress/regress1/strings/stoi-400million.smt2 index 709bd7549..1b1fca2ac 100644 --- a/test/regress/regress1/strings/stoi-400million.smt2 +++ b/test/regress/regress1/strings/stoi-400million.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp --no-produce-proofs +; COMMAND-LINE: --strings-exp --no-produce-proofs --no-jh-rlv-order ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic ALL) diff --git a/test/regress/regress2/strings/issue6057-replace-re-all.smt2 b/test/regress/regress2/strings/issue6057-replace-re-all.smt2 index 9819b75dd..269a89e61 100644 --- a/test/regress/regress2/strings/issue6057-replace-re-all.smt2 +++ b/test/regress/regress2/strings/issue6057-replace-re-all.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp +; COMMAND-LINE: --strings-exp --no-jh-rlv-order (set-logic QF_SLIA) (declare-fun literal_0 () String) (assert (and (str.<= (str.++ literal_0 "\u{2f}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2f}\u{74}\u{79}\u{70}\u{65}\u{2f}\u{6e}\u{75}\u{6d}\u{65}\u{72}\u{69}\u{63}\u{61}\u{6c}\u{2f}\u{65}\u{64}\u{69}\u{74}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2e}\u{68}\u{74}\u{6d}\u{6c}") |