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/smt/smt_engine_check_proof.cpp | |
| parent | c604492260d0555bdb3cac5ba0863b7223f21777 (diff) | |
Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).
Diffstat (limited to 'src/smt/smt_engine_check_proof.cpp')
| -rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index 2080c772a..4c35bd863 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -57,9 +57,10 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << endl; - if( ! ( d_logic.isPure(theory::THEORY_BOOL) || - ( d_logic.isPure(theory::THEORY_UF) && - ! d_logic.hasCardinalityConstraints() ) ) ) { + if( !(d_logic.isPure(theory::THEORY_BOOL) || + (d_logic.isPure(theory::THEORY_UF) && + ! d_logic.hasCardinalityConstraints())) || + d_logic.isQuantified()) { // no checking for these yet Notice() << "Notice: no proof-checking for non-UF/Bool proofs yet" << endl; return; |