diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-22 00:50:02 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-22 07:50:02 +0000 |
| commit | d3af203110d575a89a119c4f2c3956a4f6ce69f5 (patch) | |
| tree | 865ff8ba65e9ea03008680a493091d0ba4a441b6 /src/smt/set_defaults.cpp | |
| parent | b839049634d97025ac57ba9a342fd8ab70737a33 (diff) | |
Add support for minimal unsat cores (#4605)
This commit adds support for computing minimal unsat cores. The
algorithm implemented in this commit is just a trivial deletion-based
algorithm that tries to remove each assertion in the unsat core
individually.
Diffstat (limited to 'src/smt/set_defaults.cpp')
| -rw-r--r-- | src/smt/set_defaults.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index bb104e98d..d5b3b7929 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -69,7 +69,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.driver.dumpUnsatCores = true; } if (options::checkUnsatCores() || options::dumpUnsatCores() - || options::unsatAssumptions() + || options::unsatAssumptions() || options::minimalUnsatCores() || options::unsatCoresMode() != options::UnsatCoresMode::OFF) { opts.smt.unsatCores = true; |