kdrag.theories.bitvec.BitVecSort

kdrag.theories.bitvec.BitVecSort(N)
>>> BV32 = BitVecSort(32)
>>> BV32.bvadd_comm
|= ForAll([x, y], x + y == y + x)