Approximate SMT Counting Beyond Discrete Domains

Researchers introduce pact, a new SMT model counter that can handle hybrid formulas containing both discrete and continuous variables using hashing-based approximate counting. The tool significantly outperforms existing baselines, successfully processing 456 out of 3119 test instances compared to only 83 for the baseline method.