diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-03-16 12:19:46 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-16 15:19:46 +0000 |
| commit | 0d3ea6f2dcaf80d386c7765ee8a708c18e3ed574 (patch) | |
| tree | 6dbc58a39c468cc0ab96ab7b8928a6de223333a9 /src/prop/minisat | |
| parent | 5a879f4315d0105f8487c8718659a4f060ea634e (diff) | |
[proof-new] Renaming proof option to be in sync with SMT-LIB (#6154)
Diffstat (limited to 'src/prop/minisat')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 | ||||
| -rw-r--r-- | src/prop/minisat/minisat.cpp | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index b36fe9517..8c27e2bdd 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -56,7 +56,7 @@ namespace { */ bool assertionLevelOnly() { - return (options::proof() || options::unsatCores()) + return (options::produceProofs() || options::unsatCores()) && options::incrementalSolving(); } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 935c08e9b..694c73e5e 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -160,7 +160,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { } d_minisat->addClause(minisat_clause, removable, clause_id); // FIXME: to be deleted when we kill old proof code for unsat cores - Assert(!options::unsatCores() || options::proof() + Assert(!options::unsatCores() || options::produceProofs() || clause_id != ClauseIdError); return clause_id; } |