diff options
Diffstat (limited to 'src/theory/uf/proof_equality_engine.h')
| -rw-r--r-- | src/theory/uf/proof_equality_engine.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 314353131..e1105623a 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -180,6 +180,8 @@ class ProofEqEngine : public EagerProofGenerator const std::vector<Node>& args); /** Multi-step version */ TrustNode assertConflict(const std::vector<Node>& exp, ProofStepBuffer& psb); + /** Generator version, where pg has a proof of false from assumptions exp */ + TrustNode assertConflict(const std::vector<Node>& exp, ProofGenerator* pg); //-------------------------- assert lemma /** * Called when we have concluded conc, typically via theory specific |