diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp
index 24841016c..fdbf768aa 100644
--- a/src/ast/proofs/proof_checker.cpp
+++ b/src/ast/proofs/proof_checker.cpp
@@ -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: