summaryrefslogtreecommitdiff
path: root/test/system/boilerplate.cpp
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2020-06-29 15:35:44 -0700
committerGitHub <noreply@github.com>2020-06-29 17:35:44 -0500
commit19054b3b1d427e662d30d4322df2b2f2361353da (patch)
tree1ee878fd6c2c36b78ea33607a5668e6a6d8f7144 /test/system/boilerplate.cpp
parent5cd6f0e5e910ad61ebc5045170842078818a3b80 (diff)
Make ExprManager constructor private (#4669)
This commit makes the ExprManager constructor private and updates the initialization of subsolvers, unit tests, and system tests accordingly. This is a step towards making options part of SmtEngine instead of NodeManager.
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