class

Z3::BitvecSort

Inherits Reference < Object

Constructors

new(size : UInt32)

Instance methods

==(other : BitvecSort)

Z3 hash-conses its sorts, so two Bitvec sorts of the same size are one sort

[](expr : BitvecExpr)

[](v : Int)

cast(value) : BitvecExpr

from_ast(ast : LibZ3::Ast) : BitvecExpr

size

to_s(io)

to_unsafe

var(name : String)