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, and Example 21 from our paper.

Detailed Results

Here, we provide a table with detailed results of our evaluation. For instances that could only be solved by a single configuration of SwInE, the corresponding result is highlighted in yellow.