diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-12 18:24:54 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-16 22:28:26 -0500 |
| commit | 5186ca79710fe935d1f7ed27c4a34e913ab547e8 (patch) | |
| tree | 4f5ce4957063085f607492a6474b0d244e4b2da4 /src/smt/smt_engine.cpp | |
| parent | 4d9caf9782c59823fb95519b9b518b7d7f89738a (diff) | |
First attempt at incorporating LFSC proof checker into CVC4.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0fadca424..1f83bb547 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3358,6 +3358,12 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc checkModel(/* hard failure iff */ ! r.isUnknown()); } } + // Check that UNSAT results generate a proof correctly. + if(options::checkProofs()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + checkProof(); + } + } return r; }/* SmtEngine::checkSat() */ @@ -3428,6 +3434,12 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept checkModel(/* hard failure iff */ ! r.isUnknown()); } } + // Check that UNSAT results generate a proof correctly. + if(options::checkProofs()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + checkProof(); + } + } return r; }/* SmtEngine::query() */ |