mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix c++
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7a6070506d
commit
e0d6e04493
|
@ -3799,6 +3799,7 @@ namespace z3 {
|
||||||
}
|
}
|
||||||
inline expr re_diff(expr const& a, expr const& b) {
|
inline expr re_diff(expr const& a, expr const& b) {
|
||||||
check_context(a, b);
|
check_context(a, b);
|
||||||
|
context& ctx = a.ctx();
|
||||||
Z3_ast r = Z3_mk_re_diff(ctx, a, b);
|
Z3_ast r = Z3_mk_re_diff(ctx, a, b);
|
||||||
ctx.check_error();
|
ctx.check_error();
|
||||||
return expr(ctx, r);
|
return expr(ctx, r);
|
||||||
|
|
Loading…
Reference in a new issue