diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-09 13:53:06 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-09 13:53:06 -0500 |
| commit | 6bdea0970f018639b6c4173c0eab4d05273b4ab3 (patch) | |
| tree | 8be2a06a88290608f53404e0577366edf923e799 | |
| parent | 2f8caabd570dd5bb2936d9f094b7b302a510aa6d (diff) | |
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.
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 |
1 files changed, 2 insertions, 1 deletions
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 ) |