diff options
Diffstat (limited to 'src/theory/strings/infer_proof_cons.cpp')
| -rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 34597c8be..5eba8663a 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -59,6 +59,11 @@ void InferProofCons::notifyFact(const InferInfo& ii) d_lazyFactMap.insert(ii.d_conc, iic); } +void InferProofCons::notifyLemma(const InferInfo& ii) +{ + d_lazyFactMap[ii.d_conc] = std::make_shared<InferInfo>(ii); +} + bool InferProofCons::addProofTo(CDProof* pf, Node conc, InferenceId infer, |