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.

diff --git a/test/regress/regress1/strings/stoi-400million.smt2 b/test/regress/regress1/strings/stoi-400million.smt2
index 709bd7549bac39f9375a4d340147a29a1c92744a..1b1fca2ac095d7590db408d9be7d5f6c47743198 100644 (file)
--- 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 9819b75dd6a35a7bb0d452c2cd0483e5492616fc..269a89e618639412c4ba35074d87f7e50eb74884 100644 (file)
--- 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}")