diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index df6230420..cb5235085 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -4095,7 +4095,7 @@ def BV2Int(a, is_signed=False):
     >>> x > BV2Int(b, is_signed=True)
     x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
     >>> solve(x > BV2Int(b), b == 1, x < 3)
-    [x = 2, b = 1]
+    [b = 1, x = 2]
     """
     if z3_debug():
         _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")