Benchmarks for Model Counting Modulo The Theory of Bit-vector
There benchmarks are path conditions (PCs) gathered by Symbolic PathFinder.
- ModMulBigInteger: generated from the Modulo Multiplication program in Gabfeed1.
- ModPowlBigInteger: generated from the Modulo Exponentiation program in Gabfeed1.
- ModPowReduction: generated from another Modulo Exponenation program in our paper. Different from other benchmarks, each file is a set of PCs, by changing the assertion for the PCs in a file, you can obtain a new benchmark.