From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 14 Dec 2013 00:46:01 +0000 (-0500)
Subject: Another fix for clang.
X-Git-Tag: cvc5-1.0.0~6987^2~32
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f00388be05d459a9db4db359d602317bc7e1f3b9;p=cvc5.git

Another fix for clang.
---

diff --git a/examples/hashsmt/sha1smt.cpp b/examples/hashsmt/sha1smt.cpp
index 1bdd380c1..720ef52b4 100644
--- a/examples/hashsmt/sha1smt.cpp
+++ b/examples/hashsmt/sha1smt.cpp
@@ -54,8 +54,8 @@ int main(int argc, char* argv[]) {
     output << SetBenchmarkLogicCommand("QF_BV") << endl;
     output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl;
 
-    // Make the variables the size of the string    
-    hashsmt::cvc4_uchar8 cvc4input[msgSize];
+    // Make the variables the size of the string
+    hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[msgSize];
     for (unsigned i = 0; i < msgSize; ++ i) {
       stringstream ss;
       ss << "x" << i; 
@@ -70,17 +70,17 @@ int main(int argc, char* argv[]) {
     // Do the cvc4 encoding
     hashsmt::sha1 cvc4encoder;
     cvc4encoder.process_bytes(cvc4input, msgSize);
-    
+
     // Get the digest as bitvectors
     hashsmt::cvc4_uint32 cvc4digest[5];
     cvc4encoder.get_digest(cvc4digest);
-                
+
     // Do the actual sha1 encoding
     boost::uuids::detail::sha1 sha1encoder;
     sha1encoder.process_bytes(msg.c_str(), msgSize);
     unsigned sha1digest[5];
     sha1encoder.get_digest(sha1digest);
-                
+
     // Create the assertion
     Expr assertion;
     for (unsigned i = 0; i < 5; ++ i) {
@@ -92,10 +92,12 @@ int main(int argc, char* argv[]) {
       }
     }
     output << AssertCommand(assertion) << endl;
-    
+
     // Checksat command
     output << CheckSatCommand() << endl;
-                
+
+    delete cvc4input;
+
   } catch (CVC4::Exception& e) {
     cerr << e << endl;
   }