From 4e9b76365d40882318c32e64682b96e80415b95a Mon Sep 17 00:00:00 2001 From: Yan Date: Mon, 16 Nov 2015 15:41:12 -0800 Subject: [PATCH] pass the correct context into And() when doing Tactic.as_expr() --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 214d8b687..444c025e6 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -4862,7 +4862,7 @@ class Goal(Z3PPObject): elif sz == 1: return self.get(0) else: - return And([ self.get(i) for i in range(len(self)) ]) + return And([ self.get(i) for i in range(len(self)) ], self.ctx) ######################################### #