Documentation

Given an array, and bounds on it, initialize it within the bounds to the element given. Otherwise, leave it untouched.

Prove a simple property: If we read from the initialized region, we get the initial value. We have:

>>> memsetExample
Q.E.D.

Get an example of reading a value out of range. The value returned should be out-of-range for lo/hi

>>> outOfInit
Satisfiable. Model:
  Read = 1 :: Integer
  lo   = 0 :: Integer
  hi   = 0 :: Integer
  zero = 0 :: Integer
  idx  = 1 :: Integer