From f4894f5e0630bd3610699b13a8abae3e0ce9e600 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 28 May 2021 07:10:15 -0700 Subject: [PATCH] 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. --- test/regress/regress1/strings/stoi-400million.smt2 | 2 +- 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}") -- 2.30.2