diff options
author | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
---|---|---|
committer | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
commit | 3395c5c13cd61d98aec0d9806e3b9bc3d707968a (patch) | |
tree | 0eadad9799862ec77d29f7abe03a46c300d80de8 /proofs | |
parent | 773e7d27d606b71ff0f78e84efe1deef2653f016 (diff) | |
parent | 5f415d4585134612bc24e9a823289fee35541a01 (diff) |
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
Conflicts:
src/options/quantifiers_options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/lfsc_checker/expr.h | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h index 5a505a3d9..a461e847c 100644 --- a/proofs/lfsc_checker/expr.h +++ b/proofs/lfsc_checker/expr.h @@ -88,7 +88,9 @@ protected: : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class) { } -public: + public: + virtual ~Expr() {} + static int markedCount; inline Expr* followDefs(); inline int getclass() const { return data & 7; } @@ -181,7 +183,7 @@ public: C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H(CExpr,kids); Expr **kids; - ~CExpr() { + virtual ~CExpr() { delete[] kids; } CExpr(int _op) : Expr(CEXPR, _op), kids() { @@ -261,7 +263,7 @@ public: class IntExpr : public Expr { public: mpz_t n; - ~IntExpr() { + virtual ~IntExpr() { mpz_clear(n); } IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() { @@ -280,7 +282,7 @@ class IntExpr : public Expr { class RatExpr : public Expr { public: mpq_t n; - ~RatExpr() { + virtual ~RatExpr() { mpq_clear(n); } RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() { @@ -321,6 +323,9 @@ class SymExpr : public Expr { debugrefcnt(1,CREATE); #endif } + + virtual ~SymExpr() {} + #ifdef MARKVAR_32 private: int mark(); @@ -349,6 +354,8 @@ class SymSExpr : public SymExpr { debugrefcnt(1,CREATE); #endif } + + virtual ~SymSExpr() {} }; class HoleExpr : public Expr { |