From aec8000bdaea84ca377fcd00809b4e1e8cf096b8 Mon Sep 17 00:00:00 2001
From: pinzaghi <51960393+pinzaghi@users.noreply.github.com>
Date: Mon, 29 Jun 2020 18:59:10 +0200
Subject: [PATCH] in check method, as_ast() call fails when True passed as
 assumption (#4550)

---
 src/api/python/z3/z3.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 5729fd68e..4ea15895a 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6670,11 +6670,12 @@ class Solver(Z3PPObject):
         >>> s.check()
         unknown
         """
+        s = BoolSort(self.ctx)
         assumptions = _get_args(assumptions)
         num = len(assumptions)
         _assumptions = (Ast * num)()
         for i in range(num):
-            _assumptions[i] = assumptions[i].as_ast()
+            _assumptions[i] = s.cast(assumptions[i]).as_ast()
         r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
         return CheckSatResult(r)