From 9667185af0e0e96c36f364a42247aef4691dc471 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Apr 2016 12:53:50 +0200 Subject: [PATCH] issue #549, replace BoolVal by False, otherwise creates regression Signed-off-by: Nikolaj Bjorner --- 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 b2c96965f..211b6777e 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -797,7 +797,7 @@ class ExprRef(AstRef): False """ if other == None: - return BoolVal(False, self.ctx) + return False a, b = _coerce_exprs(self, other) return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)