From 2841796a92dbd5b38228c6b87e401eb19a2efdff Mon Sep 17 00:00:00 2001
From: Henrich Lauko <xlauko@mail.muni.cz>
Date: Wed, 14 Oct 2020 06:24:12 +0200
Subject: [PATCH] z3++: add missing fpa operator >= implementation (#4729)

---
 src/api/c++/z3++.h | 3 +++
 1 file changed, 3 insertions(+)

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