diff options
Diffstat (limited to 'src/theory/builtin/proof_checker.cpp')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 1309a05f9..d5b856456 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -57,6 +57,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3); pc->registerTrustedChecker(PfRule::THEORY_INFERENCE, this, 3); + pc->registerChecker(PfRule::ALETHE_RULE, this); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( |