diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-05-19 10:58:12 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-05-19 10:58:12 -0700 |
| commit | 1b2b10afd800b90eed5ffb6e6614b2c8cfd2a4ba (patch) | |
| tree | 129a872763fb6ab32b10d8dea654f0826279f3b5 | |
| parent | b5afe6de8eecde0c70239219fdc060d7ef47b663 (diff) | |
Minor
| -rw-r--r-- | src/theory/builtin/proof_checker.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 219b50db8..c8241200d 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -74,9 +74,9 @@ class BuiltinProofRuleChecker : public ProofRuleChecker */ static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE); /** - * Apply small-step rewrite on n (either pre- or post-rewrite). This - * encapsulates the exact behavior of a THEORY_REWRITE step in a proof. - * Rewriting is performed on the Skolem form of n. + * Apply small-step rewrite on n in witness form (either pre- or + * post-rewrite). This encapsulates the exact behavior of a THEORY_REWRITE + * step in a proof. Rewriting is performed on the Skolem form of n. * * @param n The node (in witness form) to rewrite * @param preRewrite If true, performs a pre-rewrite or a post-rewrite |