This module provides the implementation of the bv_decide family of tactics in sym => mode.