diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-02-07 18:53:15 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-02-07 18:53:15 -0800 |
| commit | 264f1bee97fd299e19ef6d99271c75031b6cbd6a (patch) | |
| tree | 606f432d3c1f9dc926b6d95e93a95217b0c1a5e6 /src/include/cvc4_private_library.h | |
| parent | 0f24023a582da003e4a23fb285e66f3f41b2a842 (diff) | |
Make "unknown" non-critical for unsat cores check
Fixes #3480. Fixes #3655. `--check-unsat-cores` was failing when we got
`unknown` as an answer. However, for undecidable theories, we cannot
guarantee that we will be able to determine that the unsat core by
itself is `unsat`. This commit weakens the check to emit a warning
instead of an error when the answer is `unknown`.
Diffstat (limited to 'src/include/cvc4_private_library.h')
0 files changed, 0 insertions, 0 deletions