From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 21 May 2018 18:00:44 +0000 (+0300)
Subject: Fix compiler warning in hashsmt example (#1927)
X-Git-Tag: cvc5-1.0.0~5033
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=355dcf6675673b7b671a6452b56a29c7663882dc;p=cvc5.git

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).
---

diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index 1a99ee406..8704b582f 100644
--- a/examples/hashsmt/sha1_inversion.cpp
+++ b/examples/hashsmt/sha1_inversion.cpp
@@ -27,6 +27,7 @@
 #include <iostream>
 #include <sstream>
 #include <string>
+#include <vector>
 
 #include "expr/expr_iomanip.h"
 #include "options/language.h"
@@ -57,7 +58,7 @@ int main(int argc, char* argv[]) {
     output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl;
 
     // Make the variables the size of the string
-    hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[msgSize];
+    std::vector<hashsmt::cvc4_uchar8> cvc4input(msgSize);
     for (unsigned i = 0; i < msgSize; ++ i) {
       stringstream ss;
       ss << "x" << i;
@@ -71,7 +72,7 @@ int main(int argc, char* argv[]) {
 
     // Do the cvc4 encoding
     hashsmt::sha1 cvc4encoder;
-    cvc4encoder.process_bytes(cvc4input, msgSize);
+    cvc4encoder.process_bytes(cvc4input.data(), msgSize);
 
     // Get the digest as bitvectors
     hashsmt::cvc4_uint32 cvc4digest[5];
@@ -97,9 +98,6 @@ int main(int argc, char* argv[]) {
 
     // Checksat command
     output << CheckSatCommand() << endl;
-
-    delete cvc4input;
-
   } catch (CVC4::Exception& e) {
     cerr << e << endl;
   }