Fix use-after-free with ResChains

This commit fixes an issue where the ResChain in `d_resolutionChains` gets
deleted here:

https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L729

The condition immediately after is false because the condition on line 727 is
true. Thus, `d_resolutionChains` now has a deleted entry for `id`.

When CVC4 afterwards gets the ResChain associated with `id` in
`checkResolution()`, it accesses the deleted entry:

https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L303

diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index bcc849906ee870b2d5ca3fe3c30b6e6a1ef1450b..eb4e04d1336796f6b36f0974adb66e98e42edf51 100644 (file)
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -728,8 +728,8 @@ void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* res) {
     ResChain<Solver>* current = (*d_resolutionChains.find(id)).second;
     delete current;
   }
-  if (d_resolutionChains.find(id) == d_resolutionChains.end())
-    d_resolutionChains.insert(id, res);
+
+  d_resolutionChains.insert(id, res);
 
   if (Debug.isOn("proof:sat")) {
     printRes(id);