From ddbe17d581d9835f9bc57079383eefce2b841162 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Apr 2022 16:08:54 +0200 Subject: [PATCH] #5965 define the is_bool on ArithSortRef --- src/api/python/z3/z3.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index d3d6067c3..223b3e038 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2279,6 +2279,9 @@ class ArithSortRef(SortRef): """ return self.kind() == Z3_INT_SORT + def is_bool(self): + return False + def subsort(self, other): """Return `True` if `self` is a subsort of `other`.""" return self.is_int() and is_arith_sort(other) and other.is_real()