diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
| commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
| tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /src/smt/smt_engine_check_proof.cpp | |
| parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) | |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/smt/smt_engine_check_proof.cpp')
| -rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index c4747d724..14adcc536 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -64,11 +64,12 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << endl; if( !(d_logic.isPure(theory::THEORY_BOOL) || + d_logic.isPure(theory::THEORY_BV) || (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; + Notice() << "Notice: no proof-checking for non-UF/Bool/BV proofs yet" << endl; return; } @@ -91,7 +92,7 @@ void SmtEngine::checkProof() { a.use_nested_app = false; a.compile_lib = false; init(); - check_file(pfFile, args()); + check_file(pfFile, a); close(fd); #else /* IS_PROOFS_BUILD */ |