From 0e32c87dc385d086382227b1b9470fa0b750b4a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 May 2015 15:43:05 +0100 Subject: [PATCH] fix examples and C++ API - build failure Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.cpp | 2 +- src/api/c++/z3++.h | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index 2a90b5a3f..d40aa93e9 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -2083,7 +2083,7 @@ bool parse_is_sat_line(char const* line, bool& is_sat) { return true; } return false; - +} bool parse_is_sat(char const* filename, bool& is_sat) { std::ifstream is(filename); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 11c80a2be..3c925e95c 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1111,7 +1111,8 @@ namespace z3 { } inline expr concat(expr const& a, expr const& b) { - Z3_ast r = Z3_mk_concat(ctx, (Z3_app) a, (Z3_app) b); + context& ctx = a.ctx(); + Z3_ast r = Z3_mk_concat(ctx, (Z3_ast) a, (Z3_ast) b); ctx.check_error(); return expr(ctx, r); }