Add virtual destructors where missing

diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 362a9fb9008b85fad6e86b3846647a715d6a9fe6..e7e8f65b69b2fb97f84ed8fe49bbbb5085b9e398 100644 (file)
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -137,6 +137,7 @@ protected:
   bool d_storedUnitConflict;
 public:  
   SatProof(::Minisat::Solver* solver, bool checkRes = false);
+  virtual ~SatProof() {}
 protected:
   void print(ClauseId id); 
   void printRes(ClauseId id);

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 7734286338758a7255e89c4b2d7ca44bb5ebb1af..b8963c50070ebfe59f9caf043de27711f4cf4258 100644 (file)
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -28,9 +28,9 @@
 
 namespace CVC4 {
 
-
   typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; 
   typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; 
+
   class TheoryProof {
   protected:
     ExprSet d_termDeclarations;
@@ -40,6 +40,7 @@ namespace CVC4 {
     void addDeclaration(Expr atom); 
   public:
     TheoryProof();
+    virtual ~TheoryProof() {}
     virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0;
   };
 
@@ -51,4 +52,5 @@ namespace CVC4 {
     virtual void printAssertions(std::ostream& os, std::ostream& paren);
   }; 
 } /* CVC4 namespace */
+
 #endif /* __CVC4__THEORY_PROOF_H */