This set of code is intended to demonstrate that a naive encoding of finite-field operations into integer or bit-vector operations is highly inefficient. 
For example, a finite-field multiplication constraint:
xF_p * yF_p == zF_p 
is modeled as 
(x * y) % p == z

We selected six simple Circom programs, instantiated from templates in Circomlib, which implement basic logic gates such as AND and OR over signals.

We manually constructed SMT models for checking both constraint equivalence and computation equivalence for these compilation instances, including versions for both Z3 and CVC5. The solver versions used are Z3（v4.15.3.0） and CVC5 (v1.2.0).

Our CirTV tool can complete both checks within tens of milliseconds, whereas the naive approach cannot finish within a reasonable time limit (10 min). More specifically, when using CVC5, none of the checks can be completed. When using Z3, due to its relatively aggressive search strategy for modular arithmetic, it can complete constraint equivalence checking (which involves fewer constraints) within milliseconds. However, for computation equivalence checking, it still results in a timeout.