From ead970b4778330768e64a04f13a46289f974cb85 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 26 Oct 2016 14:08:33 +0100 Subject: [PATCH] Bugfix for Python API. Thanks to John D. Ramsdell for reporting this issue (http://stackoverflow.com/questions/39584779/why-is-the-sort-of-a-bound-variable-forced-not-to-be-a-finite-domain-sort). --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 514a45fc6..b9d7f6df0 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1817,7 +1817,7 @@ class QuantifierRef(BoolRef): """ if __debug__: _z3_assert(idx < self.num_vars(), "Invalid variable idx") - return SortRef(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx) + return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx) def children(self): """Return a list containing a single element self.body()