From 6bdea0970f018639b6c4173c0eab4d05273b4ab3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 9 Apr 2020 13:53:06 -0500 Subject: [PATCH] Disable slow sygus regression (#4232) A regress2 SyGuS benchmark is taking 110 seconds in production on my machine. This was likely caused by the recent update v1 -> v2, which impacts the internal representation and hence the search. Disabling for now. --- test/regress/CMakeLists.txt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c5dbd38f8..8aae1890d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2058,7 +2058,6 @@ set(regress_2_tests regress2/sygus/ex23.sy regress2/sygus/examples-deq.sy regress2/sygus/icfp_easy_mt_ite.sy - regress2/sygus/inv_gen_n_c11.sy regress2/sygus/issue4022-conjecture-gen.smt2 regress2/sygus/lustre-real.sy regress2/sygus/max2-univ.sy @@ -2418,6 +2417,8 @@ set(regression_disabled_tests regress2/nl/nt-lemmas-bad.smt2 regress2/quantifiers/ForElimination-scala-9.smt2 regress2/quantifiers/small-bug1-fixpoint-3.smt2 + # currently slow at 24357fea + regress2/sygus/inv_gen_n_c11.sy regress2/xs-11-20-5-2-5-3.smtv1.smt2 regress2/xs-11-20-5-2-5-3.smt2 ) -- 2.30.2