diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-10 18:34:44 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-10 18:35:15 -0400 |
| commit | 9042fc86692b6dc67ed5ba6bd721752d9a5c5389 (patch) | |
| tree | 12cd2743b15b3af1a320ad3403668cfd5feae3b6 /src | |
| parent | 6ae07a91cdd4f20f8fdccd7e31d217c6ca34ee45 (diff) | |
Fix the build; --check-proof works for UF but not for the new UFC logic.
Diffstat (limited to 'src')
| -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 a731ff024..4c218b48c 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -57,10 +57,11 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << endl; - if(!d_logic.isPure(theory::THEORY_BOOL) && - !d_logic.isPure(theory::THEORY_UF)) { + if( ! ( d_logic.isPure(theory::THEORY_BOOL) || + ( d_logic.isPure(theory::THEORY_UF) && + ! d_logic.hasCardinalityConstraints() ) ) ) { // no checking for these yet - Notice() << "Notice: no proof-checking for non-UF proofs yet" << endl; + Notice() << "Notice: no proof-checking for non-UF/Bool proofs yet" << endl; return; } |