diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-07 22:40:15 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-07 22:40:15 -0800 |
| commit | f9e3aee4d497e3981fd4802d4b987b7c60a93719 (patch) | |
| tree | e2c3b5fcea37fa2977e9ae5dfd9c4ceea2022f44 /test/regress/regress1/sygus-abduct-test-ccore.smt2 | |
| parent | 5fa459b1bfedecb141131ade26ca51e671c38c0c (diff) | |
[Regressions] Require proof support for abductionfixNightliesNoProof
PR #3255 introduced a new feature for more scalable
abduction/interpolation that relies on unsat cores. The regressions
added in the PR were not marked as requiring proof support, however,
leading to failing builds if proof support was not enabled.
Diffstat (limited to 'test/regress/regress1/sygus-abduct-test-ccore.smt2')
| -rw-r--r-- | test/regress/regress1/sygus-abduct-test-ccore.smt2 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/sygus-abduct-test-ccore.smt2 index 86f5fe133..adb38add0 100644 --- a/test/regress/regress1/sygus-abduct-test-ccore.smt2 +++ b/test/regress/regress1/sygus-abduct-test-ccore.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: proof ; COMMAND-LINE: --produce-abducts --sygus-core-connective ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 |