projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
7803127
)
Further fix #6453 (#6804)
author
Ouyancheng
<1024842937@qq.com>
Mon, 28 Jun 2021 19:10:55 +0000
(12:10 -0700)
committer
GitHub
<noreply@github.com>
Mon, 28 Jun 2021 19:10:55 +0000
(19:10 +0000)
There's one spot left in issue #6453, that is the call to `std::allocator<T>::destroy` in `mkMetaKind`. And this commit fixes it.
src/expr/mkmetakind
patch
|
blob
|
history
diff --git
a/src/expr/mkmetakind
b/src/expr/mkmetakind
index 88208d77690d9157af9478485323132e5a3a6083..f9b49fc0acd994397fbc30b4661c2f077254cf3a 100755
(executable)
--- 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;
"
}