Fix use-after-free in eager bitblaster (#1772)

There was a use-after-free in the eager bitblaster: the context used by
the SAT solver was destroyed before the solver. This lead to a
use-after-free in the destructor of the SAT solver when destroying
context-dependent objects. This commit fixes the issue by changing the
desctruction order such that the context is destroyed after the SAT
solver.

Note: This issue was introduced in commit
a917cc2ab4956b542b1f565abf0e62b197692f8d because d_nullContext and
d_satSolver were changed to be std::unique_ptrs.

1 files changed, 2 insertions, 1 deletions

diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index 8610d0181..bea275c67 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -55,11 +55,12 @@ class EagerBitblaster : public TBitblaster<Node>
   void setProofLog(BitVectorProof* bvp);
 
  private:
+  std::unique_ptr<context::Context> d_nullContext;
+
   typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
   // sat solver used for bitblasting and associated CnfStream
   std::unique_ptr<prop::SatSolver> d_satSolver;
   std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
-  std::unique_ptr<context::Context> d_nullContext;
   std::unique_ptr<prop::CnfStream> d_cnfStream;
 
   TheoryBV* d_bv;