mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

proof-checker: handle true-axiom

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-21 10:44:29 -07:00
parent 4de58a42fe
commit 9550fd1ec4
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -211,6 +211,8 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
switch(k) {
case PR_UNDEF:
return true;
case PR_TRUE:
return true;
case PR_ASSERTED:
return true;
case PR_GOAL: