From 33a0b9e350bf9ee7fb8048d0ce5c84ae57b2626c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Mar 2022 11:02:14 -0600 Subject: [PATCH] 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. --- test/regress/CMakeLists.txt | 6 ++++-- test/regress/regress1/sygus/max-limit.sy | 1 + test/regress/regress1/sygus/max-try2.sy | 1 + 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c4c85c8f0..0ca6b0775 100644 --- 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 da5b3a1a0..3031c869b 100644 --- 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 f57c3d1be..ef8df46de 100644 --- 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) -- 2.30.2