From: Ouyancheng <1024842937@qq.com>
Date: Mon, 28 Jun 2021 19:10:55 +0000 (-0700)
Subject: Further fix #6453 (#6804)
X-Git-Tag: cvc5-1.0.0~1552
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=43fffe772a89537dfecea7e63352a03b922a0fbc;p=cvc5.git

Further fix #6453 (#6804)

There's one spot left in issue #6453, that is the call to `std::allocator<T>::destroy` in `mkMetaKind`. And this commit fixes it.
---

diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 88208d776..f9b49fc0a 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -279,7 +279,7 @@ $3 const& NodeValue::getConst< $3 >() const {
   cname=`echo "$3" | awk 'BEGIN {FS="::"} {print$NF}'`
   metakind_constDeleters="${metakind_constDeleters}
   case kind::$1:
-    std::allocator< $3 >().destroy(reinterpret_cast< $3* >(nv->d_children));
+    std::destroy_at(reinterpret_cast< $3* >(nv->d_children));
     break;
 "
 }