summaryrefslogtreecommitdiff
path: root/examples/hashsmt/sha1_inversion.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'examples/hashsmt/sha1_inversion.cpp')
-rw-r--r--examples/hashsmt/sha1_inversion.cpp16
1 files changed, 7 insertions, 9 deletions
diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index fadc6ecb9..15c7d8728 100644
--- a/examples/hashsmt/sha1_inversion.cpp
+++ b/examples/hashsmt/sha1_inversion.cpp
@@ -22,16 +22,17 @@
* Author: dejan
*/
-#include <string>
+#include <boost/uuid/sha1.hpp>
#include <fstream>
#include <iostream>
#include <sstream>
+#include <string>
-#include "word.h"
+#include "options/language.h"
+#include "options/set_language.h"
#include "sha1.hpp"
#include "smt_util/command.h"
-
-#include <boost/uuid/sha1.hpp>
+#include "word.h"
using namespace std;
using namespace CVC4;
@@ -50,7 +51,7 @@ int main(int argc, char* argv[]) {
string msg = argv[1];
unsigned msgSize = msg.size();
ofstream output(argv[2]);
- output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2);
+ output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2);
output << SetBenchmarkLogicCommand("QF_BV") << endl;
output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl;
@@ -58,7 +59,7 @@ int main(int argc, char* argv[]) {
hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[msgSize];
for (unsigned i = 0; i < msgSize; ++ i) {
stringstream ss;
- ss << "x" << i;
+ ss << "x" << i;
cvc4input[i] = hashsmt::cvc4_uchar8(ss.str());
output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl;
@@ -102,6 +103,3 @@ int main(int argc, char* argv[]) {
cerr << e << endl;
}
}
-
-
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback