summaryrefslogtreecommitdiff
path: root/test/system/ouroborous.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'test/system/ouroborous.cpp')
-rw-r--r--test/system/ouroborous.cpp15
1 files changed, 8 insertions, 7 deletions
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp
index 1df405a17..a135e6c6c 100644
--- a/test/system/ouroborous.cpp
+++ b/test/system/ouroborous.cpp
@@ -2,7 +2,7 @@
/*! \file ouroborous.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Tim King, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
@@ -28,6 +28,7 @@
#include <sstream>
#include <string>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "expr/expr_iomanip.h"
#include "options/set_language.h"
@@ -108,12 +109,12 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL
int runTest() {
- ExprManager em;
- psr =
- ParserBuilder(&em, "internal-buffer")
- .withStringInput(declarations)
- .withInputLanguage(input::LANG_SMTLIB_V2)
- .build();
+ std::unique_ptr<api::Solver> solver =
+ std::unique_ptr<api::Solver>(new api::Solver());
+ psr = ParserBuilder(solver.get(), "internal-buffer")
+ .withStringInput(declarations)
+ .withInputLanguage(input::LANG_SMTLIB_V2)
+ .build();
// we don't need to execute them, but we DO need to parse them to
// get the declarations
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback