diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index b4aecc9fe35..8d84d5f3685 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -62,6 +62,10 @@ class AssertionPipeline : protected EnvObj /** * Adds an assertion/assumption to be preprocessed. * + * Note that if proofs are provided, a preprocess pass using this method + * is required to either provide a proof generator or a trust id that is not + * TrustId::UNKNOWN_PREPROCESS_LEMMA. + * * @param n The assertion/assumption * @param isInput If true, n is an input formula (an assumption in the main * body of the overall proof). @@ -91,6 +95,10 @@ class AssertionPipeline : protected EnvObj * Replaces assertion i with node n and records the dependency between the * original assertion and its replacement. * + * Note that if proofs are provided, a preprocess pass using this method + * is required to either provide a proof generator or a trust id that is not + * TrustId::UNKNOWN_PREPROCESS_LEMMA. + * * @param i The position of the assertion to replace. * @param n The replacement assertion. * @param pg The proof generator who can provide a proof of d_nodes[i] == n,