summaryrefslogtreecommitdiff
path: root/test/system/boilerplate.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'test/system/boilerplate.cpp')
-rw-r--r--test/system/boilerplate.cpp14
1 files changed, 5 insertions, 9 deletions
diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
index 93f5dceb8..315cec7bf 100644
--- a/test/system/boilerplate.cpp
+++ b/test/system/boilerplate.cpp
@@ -19,18 +19,14 @@
#include <iostream>
#include <sstream>
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
+#include "api/cvc4cpp.h"
-using namespace CVC4;
+using namespace CVC4::api;
using namespace std;
int main() {
- ExprManager em;
- Options opts;
- SmtEngine smt(&em);
- Result r = smt.checkEntailed(em.mkConst(true));
-
- return (Result::ENTAILED == r) ? 0 : 1;
+ Solver slv;
+ Result r = slv.checkEntailed(slv.mkBoolean(true));
+ return r.isEntailed() ? 0 : 1;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback