Disable unsat cores in timeout regression (#4713)

Fixes a timeout in the nightlies.

One regression times out during unsat core checking. This appears to be random, the subcall to check for unsat-cores is applying sygus-inst in the expected way, however, it struggles to find the right instances.

Furthermore note that we are planning to redo implementation of unsat cores soon (when proof-new is fully merged), so we should revisit this (and all other) regressions with --no-check-unsat-cores when that happens.

diff --git a/test/regress/regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2 b/test/regress/regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
index 6ff292a3f02c2c37cad247f0e3e609fa36c5f7c9..23b4c8cbd91236d8bb6cf57976375091c82e8b71 100644 (file)
--- a/test/regress/regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
+++ b/test/regress/regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
@@ -1,4 +1,6 @@
-; COMMAND-LINE: --sygus-inst
+; COMMAND-LINE: --sygus-inst --no-check-unsat-cores
+
+; times out during unsat core checking since 6b673474
 (set-info :smt-lib-version 2.6)
 (set-logic UFBV)
 (set-info :source |