From 9550fd1ec4d7fbae30e99ef18a9a4b55bcf422db Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 21 May 2018 10:44:29 -0700
Subject: [PATCH] proof-checker: handle true-axiom

---
 src/ast/proofs/proof_checker.cpp | 2 ++
 1 file changed, 2 insertions(+)

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: