mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

fix context sensitivity. Codeplex issue 148, thanks to clockish

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-12-03 08:55:14 +09:00
parent 61c59fb4bf
commit 45755bbd14
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -6166,7 +6166,7 @@ class Fixedpoint(Z3PPObject):
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name) Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
else: else:
body = _get_args(body) body = _get_args(body)
f = self.abstract(Implies(And(body),head)) f = self.abstract(Implies(And(body, self.ctx),head))
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name) Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def rule(self, head, body = None, name = None): def rule(self, head, body = None, name = None):
@ -6194,7 +6194,7 @@ class Fixedpoint(Z3PPObject):
if sz == 1: if sz == 1:
query = query[0] query = query[0]
else: else:
query = And(query) query = And(query, self.ctx)
query = self.abstract(query, False) query = self.abstract(query, False)
r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast()) r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
return CheckSatResult(r) return CheckSatResult(r)
@ -6213,7 +6213,7 @@ class Fixedpoint(Z3PPObject):
name = "" name = ""
name = to_symbol(name, self.ctx) name = to_symbol(name, self.ctx)
body = _get_args(body) body = _get_args(body)
f = self.abstract(Implies(And(body),head)) f = self.abstract(Implies(And(body, self.ctx),head))
Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name) Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def get_answer(self): def get_answer(self):