A verificação formal é uma área de pesquisa que visa garantir a confiabilidade de sistemas críticos, como hardware e software, onde erros podem ter consequências graves. Entre as ferramentas utilizadas nesse contexto, os solucionadores SMT, como o cvc5 [1], desempenham um papel central ao permitir o raciocínio automático sobre diversas estruturas e operações, como as realizadas sobre vetores de bits, amplamente empregados em circuitos digitais. Sendo este um processo complexo, técnicas como o bit-blasting são necessárias para dividir o problema de vetores de bits em termos menores. Tradicionalmente, isso é feito com valores proposicionais, mas agora experimentamos com valores pseudo-booleanos. Este trabalho explora a integração dessas técnicas, propondo uma extensão ao formato de prova Alethe [2] e ao verificador Carcara [3], buscando maior confiança e precisão na validação de provas e seus resultados.