This directory contains the implementation and verification of the bitblaster for BitVec problems with boolean substructure. For any primitive operation defined in Basic there does exist one file in Impl, containing the bitblaster and one file in Lemmas, demonstrating that the circuit produced by the bitblaster is correct.