Fix memory leak in quantifier info (#8005)

Fixes #8001. One of the maps in `QuantInfo` was containing
heap-allocated objects that were not being destroyed. This commit
changes the raw pointers to `std::unique_ptr<MatchGen>` to avoid the
memory leak.

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index dbe141c6607304a40ac434451bc863adeea5bf4c..e1bebee740507873d56d3f66dc6103e349800f43 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -70,14 +70,14 @@ QuantInfo::QuantInfo(Env& env, QuantConflictFind* p, Node q)
          j++)
     {
       if( d_vars[j].getKind()!=BOUND_VARIABLE ){
-        d_var_mg[j] = NULL;
+        d_var_mg[j] = nullptr;
         bool is_tsym = false;
         if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){
           is_tsym = true;
           d_tsym_vars.push_back( j );
         }
         if( !is_tsym || options::qcfTConstraint() ){
-          d_var_mg[j] = new MatchGen(p, this, d_vars[j], true);
+          d_var_mg[j] = std::make_unique<MatchGen>(p, this, d_vars[j], true);
         }
         if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
           Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
@@ -280,7 +280,7 @@ bool QuantInfo::reset_round()
   d_tconstraints.clear();
 
   d_mg->reset_round();
-  for (const std::pair<const size_t, MatchGen*>& vg : d_var_mg)
+  for (const std::pair<const size_t, std::unique_ptr<MatchGen>>& vg : d_var_mg)
   {
     if (!vg.second->reset_round())
     {

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index c9cce84b905c5265aa357d0de7953ac83d8f091c..b546aacd57c83881573ae02eacd3bdcc7ef06549 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -124,7 +124,7 @@ class MatchGen {
 class QuantInfo : protected EnvObj
 {
  public:
-  typedef std::map<size_t, MatchGen*> VarMgMap;
+  using VarMgMap = std::map<size_t, std::unique_ptr<MatchGen>>;
   QuantInfo(Env& env, QuantConflictFind* p, Node q);
   ~QuantInfo();
   /** get quantified formula */

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b746102b5ff8b54f6598a46b3edcae26330f55b2..c86be3e7663817cafe4826de3cea4686c5f8ec47 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -982,6 +982,7 @@ set(regress_0_tests
   regress0/quantifiers/issue6996-trivial-elim.smt2
   regress0/quantifiers/issue6999-deq-elim.smt2
   regress0/quantifiers/issue7353-var-elim-par-dt.smt2
+  regress0/quantifiers/issue8001-mem-leak.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2

diff --git a/test/regress/regress0/quantifiers/issue8001-mem-leak.smt2 b/test/regress/regress0/quantifiers/issue8001-mem-leak.smt2
new file mode 100644 (file)
index 0000000..33695a7
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue8001-mem-leak.smt2
@@ -0,0 +1,4 @@
+; COMMAND-LINE: -q
+; EXPECT: unknown
+(assert (forall ((V (Array Int Int))) (= 0 (select V 0))))
+(check-sat)