summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-06-01 09:59:41 -0500
committerGitHub <noreply@github.com>2021-06-01 09:59:41 -0500
commit320c48b1c82feb7a5d55af39d0cdbb7a1c2c6ff2 (patch)
tree5c268c0c8ad7d568c8b0a9085e418b2c05a69e99 /test/regress
parente7dccb880f08e14004501c827cd1c199a936cb64 (diff)
Disable timeout regressions (#6650)
Disables two regressions that have been timing out causing nightlies to fail.
Diffstat (limited to 'test/regress')
-rw-r--r--test/regress/CMakeLists.txt6
1 files changed, 4 insertions, 2 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cff39938c..39f1985b0 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1785,7 +1785,6 @@ set(regress_1_tests
regress1/quantifiers/fp-cegqi-unsat.smt2
regress1/quantifiers/gauss_init_0030.fof.smt2
regress1/quantifiers/horn-simple.smt2
- regress1/quantifiers/infer-arith-trigger-eq.smt2
regress1/quantifiers/inst-max-level-segf.smt2
regress1/quantifiers/inst-prop-simp.smt2
regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
@@ -2425,7 +2424,6 @@ set(regress_2_tests
regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
regress2/javafe.ast.WhileStmt.447_no_forall.smt2
- regress2/nl/nt-lemmas-bad.smt2
regress2/nl/ufnia-factor-open-proof.smt2
regress2/ooo.rf6.smt2
regress2/ooo.tag10.smt2
@@ -2618,6 +2616,8 @@ set(regression_disabled_tests
regress1/quantifiers/anti-sk-simp.smt2
# no longer support snorm option
regress1/quantifiers/arith-snorm.smt2
+ # timeout on some builds after changes to justification heuristic
+ regress1/quantifiers/infer-arith-trigger-eq.smt2
# ajreynol: different error messages on production and debug:
regress1/quantifiers/macro-subtype-param.smt2
# times out with competition build, ok with other builds:
@@ -2663,6 +2663,8 @@ set(regression_disabled_tests
regress1/sygus/issue3498.smt2
regress2/arith/miplib-opt1217--27.smt2
regress2/nl/dumortier-050317.smt2
+ # timeout on some builds after changes to justification heuristic
+ regress2/nl/nt-lemmas-bad.smt2
# timeout after refactoring justification heuristic
regress2/ho/SYO362^5.p
# time out
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback