From 8ff3b306b7b35bc1040a6caee759929c4e497373 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 9 Jul 2020 16:07:51 -0500 Subject: [PATCH] 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. --- .../regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2 | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 6ff292a3f..23b4c8cbd 100644 --- 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 | -- 2.30.2