From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 28 May 2021 14:10:15 +0000 (-0700)
Subject: Disable `--jh-rlv-order` for slow regressions (#6633)
X-Git-Tag: cvc5-1.0.0~1679
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f4894f5e0630bd3610699b13a8abae3e0ce9e600;p=cvc5.git

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 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}")