This directory contains the implementation of the bitblaster and LRAT checker for bv_decide, as well as custom theorems used for reflection.