diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2015-04-23 17:38:48 +0100 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2015-04-23 17:38:48 +0100 |
| commit | 0daf670d46ec2e781c2060b41449f2787b6e8f66 (patch) | |
| tree | 7f1870bc621407a3c387ab6eb3dc77db529355dc /src/proof/proof_manager.h | |
| parent | c604492260d0555bdb3cac5ba0863b7223f21777 (diff) | |
Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).
Diffstat (limited to 'src/proof/proof_manager.h')
| -rw-r--r-- | src/proof/proof_manager.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 43d6723fa..ee99b0159 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -171,6 +171,7 @@ public: void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); // note that n depends on dep (for cores) void addDependence(TNode n, TNode dep); + void addUnsatCore(Expr formula); assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); } assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); } |