summaryrefslogtreecommitdiff
path: root/examples/hashsmt
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-12-13 19:46:01 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-12-13 19:46:01 -0500
commitf00388be05d459a9db4db359d602317bc7e1f3b9 (patch)
tree624d1b08eeb33e7bdd2095a968a41b7cf0e053ba /examples/hashsmt
parentc36f77919ca8e0644d66de467bb9cd614fe6a93e (diff)
Another fix for clang.
Diffstat (limited to 'examples/hashsmt')
-rw-r--r--examples/hashsmt/sha1smt.cpp16
1 files changed, 9 insertions, 7 deletions
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback