This is the evaluation of the technique from our paper “Satisfiability Modulo Exponential Integer Arithmetic”, which is implemented in our SMT solver SwInE (SMT with Integer Exponentiation). For more information abot SwInE, we refer to its website.

Downloading SwInE

Here you can find the release of SwInE that was used for our evaluation.

Input Format

SwInE supports an extension of the SMTLIB-format with an additional binary function symbol exp, whose arguments have to be of sort Int. The semantics of exp(s,t) is s^|t|.

Using SwInE

Please execute swine --help for detailed information on using SwInE.

Benchmarks

You can find the benchmarks from our evaluation here. Moreover, you can download our leading example, Example 14, and Example 25 from our paper.

Detailed Results

We provide tables with detailed results of our evaluation on the LoAT problems.

• CHC Comp '22 Problems
• CHC Comp '23 Problems
• Complexity Problems
• Termination Problems