summaryrefslogtreecommitdiff
path: root/examples/nra-translate/smt2toredlog.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'examples/nra-translate/smt2toredlog.cpp')
-rw-r--r--examples/nra-translate/smt2toredlog.cpp8
1 files changed, 4 insertions, 4 deletions
diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp
index da34ca4da..b2717c157 100644
--- a/examples/nra-translate/smt2toredlog.cpp
+++ b/examples/nra-translate/smt2toredlog.cpp
@@ -24,7 +24,7 @@ void translate_to_redlog(
const vector<string>& info_tags,
const vector<string>& info_data,
const map<Expr, unsigned>& variables,
- const vector<BoolExpr>& assertions);
+ const vector<Expr>& assertions);
int main(int argc, char* argv[])
{
@@ -50,7 +50,7 @@ int main(int argc, char* argv[])
std::map<Expr, unsigned> variables;
vector<string> info_tags;
vector<string> info_data;
- vector<BoolExpr> assertions;
+ vector<Expr> assertions;
Command* cmd;
while ((cmd = parser->nextCommand())) {
@@ -155,7 +155,7 @@ void translate_to_redlog_term(const map<Expr, unsigned>& variables, const Expr&
}
}
-void translate_to_redlog(const map<Expr, unsigned>& variables, const BoolExpr& assertion) {
+void translate_to_redlog(const map<Expr, unsigned>& variables, const Expr& assertion) {
bool first;
unsigned n = assertion.getNumChildren();
@@ -269,7 +269,7 @@ void translate_to_redlog(
const vector<string>& info_tags,
const vector<string>& info_data,
const std::map<Expr, unsigned>& variables,
- const vector<BoolExpr>& assertions)
+ const vector<Expr>& assertions)
{
bool first;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback