summaryrefslogtreecommitdiff
path: root/examples/nra-translate/smt2toisat.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'examples/nra-translate/smt2toisat.cpp')
-rw-r--r--examples/nra-translate/smt2toisat.cpp5
1 files changed, 2 insertions, 3 deletions
diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index 09b0c69d8..5898e5cff 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -15,6 +15,8 @@
** \todo document this file
**/
+#include <cvc5/cvc5.h>
+
#include <cassert>
#include <iostream>
#include <map>
@@ -22,9 +24,6 @@
#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