diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-21 21:00:44 +0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-21 21:00:44 +0300 |
| commit | 355dcf6675673b7b671a6452b56a29c7663882dc (patch) | |
| tree | 369f5a60a11f370625e1fc793d2173f15dfa5027 /test | |
| parent | bff00f51cd0d2f59262aa18ff3e217a78503ae7a (diff) | |
Fix compiler warning in hashsmt example (#1927)
Previously, we were using delete for an array allocated on the heap,
which caused a warning. @dddejan fixed this and other issues in PR #1909
but after @ajreynol fixed the other issues in a separate PR and to not
waste @dddejan's time, I am submitting this fix separately (note: the
fix is slightly different in that it changes the array to a vector,
making a delete[] unnecessary).
Diffstat (limited to 'test')
0 files changed, 0 insertions, 0 deletions