From e9315af0d90f3918a6faa0d98dc3395f239e0a19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Nov 2015 04:22:44 -0800 Subject: [PATCH] remove tabs from z3.py to fix build Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 837443e07..214d8b687 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1,3 +1,4 @@ + ############################################ # Copyright (c) 2012 Microsoft Corporation # @@ -4147,7 +4148,7 @@ def Ext(a, b): """Return extensionality index for arrays. """ if __debug__: - _z3_assert(is_array(a) and is_array(b)) + _z3_assert(is_array(a) and is_array(b)) return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast())); def is_select(a): @@ -6096,12 +6097,12 @@ class Solver(Z3PPObject): >>> c1 = Context() >>> c2 = Context() - >>> s1 = Solver(ctx=c1) - >>> s2 = s1.translate(c2) + >>> s1 = Solver(ctx=c1) + >>> s2 = s1.translate(c2) """ if __debug__: _z3_assert(isinstance(target, Context), "argument must be a Z3 context") - solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) + solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) return Solver(solver, target) def sexpr(self):