From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 9 Apr 2020 18:53:06 +0000 (-0500)
Subject: Disable slow sygus regression (#4232)
X-Git-Tag: cvc5-1.0.0~3392
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6bdea0970f018639b6c4173c0eab4d05273b4ab3;p=cvc5.git

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.
---

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
 )