From cd2701da0c83eb587a647b7b0e4f36761faa5fae Mon Sep 17 00:00:00 2001
From: pcarbonn <pierre.carbonnelle@gmail.com>
Date: Tue, 31 Aug 2021 19:01:47 +0200
Subject: [PATCH] fix the use of ctx in Q() (#5521)

* fix #4956

* fix: use ctx in Q()
---
 src/api/python/z3/z3.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 3f6dbd2e0..3f0518650 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -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):