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); }