summaryrefslogtreecommitdiff
path: root/examples/nra-translate/smt2info.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'examples/nra-translate/smt2info.cpp')
-rw-r--r--examples/nra-translate/smt2info.cpp5
1 files changed, 2 insertions, 3 deletions
diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp
index 1eb4b3d4d..413601769 100644
--- a/examples/nra-translate/smt2info.cpp
+++ b/examples/nra-translate/smt2info.cpp
@@ -15,15 +15,14 @@
** \todo document this file
**/
+#include <cvc5/cvc5.h>
+
#include <cassert>
#include <iostream>
#include <string>
#include <typeinfo>
#include <vector>
-#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
-
using namespace std;
using namespace cvc5;
using namespace cvc5::parser;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback