mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

issue #549, replace BoolVal by False, otherwise creates regression

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-03 12:53:50 +02:00
parent 11e8f06272
commit 9667185af0
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -797,7 +797,7 @@ class ExprRef(AstRef):
False False
""" """
if other == None: if other == None:
return BoolVal(False, self.ctx) return False
a, b = _coerce_exprs(self, other) a, b = _coerce_exprs(self, other)
return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)