diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-13 18:20:17 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-13 18:20:17 -0500 |
commit | 8088cf4f9c8fdd49e2f46656243efb6afce3cbc8 (patch) | |
tree | ffb3f931013e01dee56c0b96e20fc64f86e3844f /src/proof | |
parent | d5f1e40c1db973c9216a167b350a6dd5a4632761 (diff) |
Add virtual destructors where missing
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/sat_proof.h | 1 | ||||
-rw-r--r-- | src/proof/theory_proof.h | 4 |
2 files changed, 4 insertions, 1 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 362a9fb90..e7e8f65b6 100644 --- 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 773428633..b8963c500 100644 --- 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 */ |