mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Bugfix for Python API.

Browse source 
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).
This commit is contained in:
Christoph M. Wintersteiger 2016-10-26 14:08:33 +01:00
parent da4289fadc
commit ead970b477
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -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()