WASM falha na alocação de memória (std::bad_alloc)

[hbgit]

Describe the bug
Ao executar a ferramenta map2check via linha de comando para analisar um arquivo C (como aritmetica.c), a execução é abortada abruptamente com um erro de falha na alocação de memória (std::bad_alloc). O travamento ocorre logo no início da rotina, imediatamente após as mensagens de "Adopting z3 solver..." e "Started Map2Check".

To Reproduce
Steps to reproduce the behavior:

1. Prepare o ambiente no Linux Mint 22.3.
2. Faça a build da aplicação utilizando o Docker de acordo com as instruções do repositório Git, ou baixe a versão in-release diretamente.
3. No terminal, navegue até a pasta do executável e rode o comando de verificação (ex: ./map2check --check-overflow aritmetica.c).

#include <stdint.h>
#include <stdbool.h>
#include <limits.h>

// Macro para exportar as funções para o WebAssembly
#define WASM_EXPORT __attribute__((visibility("default")))

// Soma básica (vulnerável a overflow)
WASM_EXPORT int32_t soma(int32_t a, int32_t b) {
    return a + b;
}


// Soma segura com detecção lógica de overflow via MSB/Sinais
WASM_EXPORT int32_t soma_segura(int32_t a, int32_t b, bool* teve_overflow) {
    int32_t resultado = a + b;
    
    // Overflow ocorre se:
    // 1. Positivo + Positivo = Negativo
    // 2. Negativo + Negativo = Positivo
    if ((a > 0 && b > 0 && resultado < 0) || (a < 0 && b < 0 && resultado >= 0)) {
        *teve_overflow = true;
    } else {
        *teve_overflow = false;
    }
    
    return resultado;
}


// Subtração básica
WASM_EXPORT int32_t sub(int32_t a, int32_t b) {
    return a - b;
}

// Subtração segura
WASM_EXPORT int32_t sub_segura(int32_t a, int32_t b, bool* teve_overflow) {
    int32_t resultado = a - b;
    
    // Overflow ocorre se:
    // 1. Positivo - Negativo = Negativo
    // 2. Negativo - Positivo = Positivo
    if ((a >= 0 && b < 0 && resultado < 0) || (a < 0 && b > 0 && resultado >= 0)) {
        *teve_overflow = true;
    } else {
        *teve_overflow = false;
    }
    
    return resultado;
}


// Multiplicação básica
WASM_EXPORT int32_t mul(int32_t a, int32_t b) {
    return a * b;
}

// Multiplicação segura
WASM_EXPORT int32_t mul_segura(int32_t a, int32_t b, bool* teve_overflow) {
    // Promove os operandos para 64 bits para calcular o produto exato
    int64_t produto_64 = (int64_t)a * (int64_t)b;
    
    // Verifica se o resultado extrapola o intervalo de 32 bits assinados
    if (produto_64 > INT32_MAX || produto_64 < INT32_MIN) {
        *teve_overflow = true;
    } else {
        *teve_overflow = false;
    }
    
    return (int32_t)produto_64;
}

4. Veja o erro de alocação de memória std::bad_alloc no console.

Expected behavior
Esperava-se que a ferramenta concluísse a análise de código para a propriedade solicitada (overflow) e retornasse o relatório no console, sem que o processo esgotasse a memória disponível ou encerrasse de forma inesperada.

Desktop (please complete the following information):

• OS: Linux Mint 22.3
• Browser: N/A (Execução em Terminal/CLI)
• Version: Build local com Docker baseada no HEAD atual do git e versão in-release.
• CPU: AMD Ryzen 7 5700U with Radeon Graphics (16) @ 4.372GHz (Speed avg: 1150 min/max: 400/4372)
• GPU: AMD ATI 05:00.0 Lucienne
• RAM Memory: 7282MiB (~8GB)
• Armazenamento: 512GB

Additional context
O problema de std::bad_alloc sugere fortemente um vazamento de memória (memory leak) ou uma tentativa excessiva e não otimizada de alocação de recursos durante a inicialização do solver (Z3).

O comportamento foi reproduzido de forma consistente em duas máquinas diferentes. Ambas as máquinas rodavam o SO Linux Mint 22.3 e apresentavam as especificações de hardware listadas acima (como os ~8GB de RAM). A falha ocorre tanto fazendo o processo manual de build via Docker (instruções da master) quanto ao tentar usar as releases empacotadas.