diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index 95d9b35cf38..a8da7d1b42b 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -123,7 +123,7 @@ class cbmc_solver_with_propt: public cbmc_solverst::solvert
     assert(_prop!=NULL);
   }
 
-  ~cbmc_solver_with_propt()
+  virtual ~cbmc_solver_with_propt()
   {
     delete prop;
   }
@@ -157,8 +157,6 @@ class cbmc_solver_with_aigpropt: public cbmc_solver_with_propt
   ~cbmc_solver_with_aigpropt()
   {
     // delete prop before the AIG
-    delete prop;
-    prop=NULL;
     delete aig;
   }
 
@@ -189,8 +187,6 @@ class cbmc_solver_with_filet:public cbmc_solverst::solvert
   ~cbmc_solver_with_filet()
   {
     // delete the prop before the file
-    delete prop_conv_ptr;
-    prop_conv_ptr=NULL;
     delete out;
   }
 
diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h
index 35ded2a5c92..07c0c3b9acf 100644
--- a/src/cbmc/cbmc_solvers.h
+++ b/src/cbmc/cbmc_solvers.h
@@ -57,7 +57,7 @@ class cbmc_solverst:public messaget
       prop_conv_ptr = _prop_conv;
     }
 
-    ~solvert()
+    virtual ~solvert()
     {
       assert(prop_conv_ptr!=NULL);
       delete prop_conv_ptr;