diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index da94ee195..0575974c2 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1543,6 +1543,9 @@ namespace z3 { else if (a.is_bv() && b.is_bv()) { r = Z3_mk_bvsge(a.ctx(), a, b); } + else if (a.is_fpa() && b.is_fpa()) { + r = Z3_mk_fpa_geq(a.ctx(), a, b); + } else { // operator is not supported by given arguments. assert(false);