mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix the use of ctx in Q() (#5521)

Browse source 
* fix #4956

* fix: use ctx in Q()
This commit is contained in:
pcarbonn 2021-08-31 19:01:47 +02:00 committed by GitHub
parent 148cb83b0d
commit cd2701da0c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3206,7 +3206,7 @@ def Q(a, b, ctx=None):
>>> Q(3,5).sort()
Real
"""
return simplify(RatVal(a, b))
return simplify(RatVal(a, b, ctx=ctx))
def Int(name, ctx=None):
@ -10578,7 +10578,7 @@ class SeqSortRef(SortRef):
class CharSortRef(SortRef):
"""Character sort."""
def StringSort(ctx=None):