Disable timing out regressions (#8273)

Fixes several of the nightly failures.

Both benchmarks involve undecidable logics and are delicate.

Also should fix the errors involving (missing) SyGuS warnings in the nightlies, which requires competition build to be disabled.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c4c85c8f016b203e9e6dc5bb11aac89dc92b661a..0ca6b0775bc998ea6268aef39f13e92ffb963146 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1973,7 +1973,6 @@ set(regress_1_tests
   regress1/nl/poly-1025.smt2
   regress1/nl/proj-365-is-int-pi.smt2
   regress1/nl/proj-issue215.smt2
-  regress1/nl/proj-issue231.smt2
   regress1/nl/proj-issue232.smt2
   regress1/nl/proj-issue253.smt2
   regress1/nl/proj-issue279.smt2
@@ -2206,7 +2205,6 @@ set(regress_1_tests
   regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2
   regress1/quantifiers/proj-issue151-2.smt2
   regress1/quantifiers/proj-issue155.smt2
-  regress1/quantifiers/proj-issue285.smt2
   regress1/quantifiers/proj-issue295.smt2
   regress1/quantifiers/psyco-001-bv.smt2
   regress1/quantifiers/psyco-107-bv.smt2
@@ -3058,6 +3056,8 @@ set(regression_disabled_tests
   regress1/nl/NAVIGATION2.smt2
   # sat or unknown in different builds
   regress1/nl/issue3307.smt2
+  # times out on various builds
+  regress1/nl/proj-issue231.smt2
   # times out after changes to nl-ext in #8236
   regress1/nl/proj-issue251.smt2
   # slow with sygus-inference after removing anti-skolemization
@@ -3070,6 +3070,8 @@ set(regression_disabled_tests
   regress1/quantifiers/macro-subtype-param.smt2
   # times out with competition build, ok with other builds:
   regress1/quantifiers/model_6_1_bv.smt2
+  # time out on some regressions
+  regress1/quantifiers/proj-issue285.smt2
   # ajreynol: different error messages on production and debug:
   regress1/quantifiers/subtype-param-unk.smt2
   regress1/quantifiers/subtype-param.smt2

diff --git a/test/regress/regress1/sygus/max-limit.sy b/test/regress/regress1/sygus/max-limit.sy
index da5b3a1a0ec554b6b1b6d3b9d213c55e60b78a14..3031c869b96ec807175d0029587e72b3c81fa99c 100644 (file)
--- a/test/regress/regress1/sygus/max-limit.sy
+++ b/test/regress/regress1/sygus/max-limit.sy
@@ -2,6 +2,7 @@
 ; ERROR-SCRUBBER: grep -o "reconstruction to syntax failed."
 ; EXPECT-ERROR: reconstruction to syntax failed.
 ; EXPECT: unknown
+; REQUIRES: no-competition
 
 (set-logic LIA)
 

diff --git a/test/regress/regress1/sygus/max-try2.sy b/test/regress/regress1/sygus/max-try2.sy
index f57c3d1be6b1142954f5ff9716d90d1b7685a872..ef8df46debcaeb079540abea86ddea1827e363ed 100644 (file)
--- a/test/regress/regress1/sygus/max-try2.sy
+++ b/test/regress/regress1/sygus/max-try2.sy
@@ -2,6 +2,7 @@
 ; ERROR-SCRUBBER: grep -o "reconstruction to syntax failed."
 ; EXPECT-ERROR: reconstruction to syntax failed.
 ; EXPECT: unknown
+; REQUIRES: no-competition
 
 (set-logic LIA)