mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 10:30:44 +00:00
Code Activity

Merge pull request #1738 from agurfinkel/deep_space

Browse source 
Fix bug in proof checking
This commit is contained in:
Nikolaj Bjorner 2018-07-07 15:36:39 -07:00 • committed by GitHub
commit 290302dca8
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/proofs/proof_checker.cpp
View file

@ -605,6 +605,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
bool found = false; bool found = false;
for (expr* term2 : terms2) { for (expr* term2 : terms2) {
found = term1 == term2; found = term1 == term2;
if (found) break;
} }
if (!found) { if (!found) {
IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m) << "\n";); IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m) << "\n";);