From e0d6e04493006d82758a9f393853dc97e82a533d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Dec 2021 16:09:39 -0800 Subject: [PATCH] fix c++ Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 91ab6d106..7ac4eacdc 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3799,6 +3799,7 @@ namespace z3 { } inline expr re_diff(expr const& a, expr const& b) { check_context(a, b); + context& ctx = a.ctx(); Z3_ast r = Z3_mk_re_diff(ctx, a, b); ctx.check_error(); return expr(ctx, r);