mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 17:36:15 +00:00
Code Activity

z3++: add missing fpa operator >= implementation (#4729)

Browse source
This commit is contained in:
Henrich Lauko 2020-10-14 06:24:12 +02:00 • committed by GitHub
parent 72b1e8a714
commit 2841796a92
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/api/c++/z3++.h
View file

@ -1543,6 +1543,9 @@ namespace z3 {
else if (a.is_bv() && b.is_bv()) { else if (a.is_bv() && b.is_bv()) {
r = Z3_mk_bvsge(a.ctx(), a, b); 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 { else {
// operator is not supported by given arguments. // operator is not supported by given arguments.
assert(false); assert(false);