diff options
Diffstat (limited to 'src/expr/proof_checker.h')
| -rw-r--r-- | src/expr/proof_checker.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index 99c02b8dc..f04587a7d 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -77,7 +77,7 @@ class ProofRuleChecker /** * This checks a single step in a proof. It is identical to check above * except that children and args have been converted to "witness form" - * (see ProofSkolemCache). Likewise, its output should be in witness form. + * (see SkolemManager). Likewise, its output should be in witness form. * * @param id The id of the proof node to check * @param children The premises of the proof node to check. These are nodes @@ -100,6 +100,8 @@ class ProofCheckerStatistics ~ProofCheckerStatistics(); /** Counts the number of checks for each kind of proof rule */ HistogramStat<PfRule> d_ruleChecks; + /** Total number of rule checks */ + IntStat d_totalRuleChecks; }; /** A class for checking proofs */ |