mirror of
https://github.com/Z3Prover/z3
synced 2025-06-13 01:16:15 +00:00
typo
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
1244d5a22e
commit
d53fdb2848
1 changed files with 1 additions and 1 deletions
|
@ -3820,7 +3820,7 @@ def BVRedAnd(a):
|
||||||
return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
|
return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
|
||||||
|
|
||||||
def BVRedOr(a):
|
def BVRedOr(a):
|
||||||
"""Return the reduction-and expression of `a`."""
|
"""Return the reduction-or expression of `a`."""
|
||||||
if __debug__:
|
if __debug__:
|
||||||
_z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
|
_z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
|
||||||
return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
|
return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue