From 45eda4bee78c3e95cbdfbc71e8aa27b967639ab9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 May 2015 21:33:36 -0700 Subject: [PATCH] allow coercion from Boolean to Int/Real, fixes #78 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 92640b2d9..7cda4bf83 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1237,6 +1237,7 @@ class BoolSortRef(SortRef): def is_bool(self): return True + class BoolRef(ExprRef): """All Boolean expressions are instances of this class.""" def sort(self):