diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-09 16:07:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-09 16:07:51 -0500 |
| commit | 8ff3b306b7b35bc1040a6caee759929c4e497373 (patch) | |
| tree | 9be1aeed88a6f3d888066c5a758325c416a2fe20 | |
| parent | 68df2d8d6c9218fe6a9bf01d22c7dfe2abdf684d (diff) | |
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.
| -rw-r--r-- | test/regress/regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2 | 4 |
1 files changed, 3 insertions, 1 deletions
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 | |