For every logic name jSMTLIB knows about, this records whether (set-logic L) gets a plain success response -- not whether the solver can actually do anything useful in that logic. Combined from runs on: linux-arm64, linux-x86_64, macos-arm64, macos-x86_64, windows.
Versions of one solver that answered every row identically share a column.
| meaning | |
|---|---|
| Y | accepted -- the solver answered success |
| A | accepted, but this solver accepts any string, valid logic or not |
| n | rejected -- unsupported, an error, or no response |
| ? | ambiguous response, or the probe timed out |
| - | this platform ships no such solver binary |
| x | binary present but unusable on every platform that has it |
| ! | platforms disagree; see the consistency section |
7 disagreement(s) -- the same solver version reached different verdicts on different platforms.
| Solver | Logic | Verdicts by platform |
|---|---|---|
| yices2 2.6.5 | QF_NIA | rejected on windows; accepted on linux-x86_64, macos-arm64, macos-x86_64 |
| yices2 2.6.5 | QF_NRA | rejected on windows; accepted on linux-x86_64, macos-arm64, macos-x86_64 |
| yices2 2.6.5 | QF_UFNRA | rejected on windows; accepted on linux-x86_64, macos-arm64, macos-x86_64 |
| yices2 2.6.5 | QF_ANIA | rejected on windows; accepted on linux-x86_64, macos-arm64, macos-x86_64 |
| yices2 2.6.5 | QF_AUFNIA | rejected on windows; accepted on linux-x86_64, macos-arm64, macos-x86_64 |
| yices2 2.6.5 | QF_NIRA | rejected on windows; accepted on linux-x86_64, macos-arm64, macos-x86_64 |
| yices2 2.6.5 | QF_UFNIA | rejected on windows; accepted on linux-x86_64, macos-arm64, macos-x86_64 |
Present, but every probe timed out. That is one fact about the binary on that platform, not a per-logic result, so these are excluded from the consistency check and shown as x below.
| Solver | Platform |
|---|---|
| z3 4.3.1 | linux-arm64 |
| z3 4.3.2 | linux-arm64 |
A marks bitwuzla 0.9.1, z3 4.3.0, z3 4.3.1, z3 4.3.2: these accept the invalid control logic too, so they do not validate the set-logic argument at all.
| Group | Logic | alt-ergo 2.6.3 | bitwuzla 0.9.1 | cvc5 1.3.2 | smtinterpol 2.5 | yices2 2.6.5 | yices2 2.7.0 | z3 4.3.0-4.3.2 | z3 4.5.0-5.1.0 |
|---|---|---|---|---|---|---|---|---|---|
| Baseline | (default) | n | A | Y | n | n | n | A | Y |
| ALL | n | A | Y | Y | Y | Y | A | Y | |
| Official | AUFLIA | n | A | Y | Y | n | n | A | Y |
| AUFLIRA | n | A | Y | Y | n | n | A | Y | |
| AUFNIRA | n | A | Y | Y | n | n | A | Y | |
| LIA | n | A | Y | Y | Y | Y | A | Y | |
| LRA | n | A | Y | Y | Y | Y | A | Y | |
| QF_ABV | n | A | Y | Y | Y | Y | A | Y | |
| QF_AUFBV | n | A | Y | Y | Y | Y | A | Y | |
| QF_AUFLIA | n | A | Y | Y | Y | Y | A | Y | |
| QF_AX | n | A | Y | Y | Y | Y | A | Y | |
| QF_BV | n | A | Y | Y | Y | Y | A | Y | |
| QF_EIA | n | A | n | n | n | n | A | n | |
| QF_FP | n | A | Y | Y | n | n | A | Y | |
| QF_IDL | n | A | Y | Y | Y | Y | A | Y | |
| QF_LIA | n | A | Y | Y | Y | Y | A | Y | |
| QF_LRA | n | A | Y | Y | Y | Y | A | Y | |
| QF_NIA | n | A | Y | Y | ! | Y | A | Y | |
| QF_NRA | n | A | Y | Y | ! | Y | A | Y | |
| QF_RDL | n | A | Y | Y | Y | Y | A | Y | |
| QF_UF | n | A | Y | Y | Y | Y | A | Y | |
| QF_UFBV | n | A | Y | Y | Y | Y | A | Y | |
| QF_UFIDL | n | A | Y | Y | Y | Y | A | Y | |
| QF_UFLIA | n | A | Y | Y | Y | Y | A | Y | |
| QF_UFLRA | n | A | Y | Y | Y | Y | A | Y | |
| QF_UFNRA | n | A | Y | Y | ! | Y | A | Y | |
| UFLRA | n | A | Y | Y | n | n | A | Y | |
| UFNIA | n | A | Y | Y | n | n | A | Y | |
| Unofficial | ALIA | n | A | Y | Y | n | n | A | Y |
| BV | n | A | Y | Y | Y | Y | A | Y | |
| NIA | n | A | Y | Y | n | n | A | Y | |
| NRA | n | A | Y | Y | n | n | A | Y | |
| QF_ALIA | n | A | Y | Y | Y | Y | A | Y | |
| QF_ANIA | n | A | Y | Y | ! | Y | A | Y | |
| QF_AUFNIA | n | A | Y | Y | ! | Y | A | Y | |
| QF_BVFP | n | A | Y | Y | n | n | A | Y | |
| QF_LIRA | n | A | Y | Y | Y | Y | A | Y | |
| QF_NIRA | n | A | Y | Y | ! | Y | A | Y | |
| QF_UFNIA | n | A | Y | Y | ! | Y | A | Y | |
| UF | n | A | Y | Y | Y | Y | A | Y | |
| UFBV | n | A | Y | Y | n | n | A | Y | |
| UFIDL | n | A | Y | Y | n | n | A | Y | |
| UFLIA | n | A | Y | Y | n | n | A | Y | |
| UFNRA | n | A | Y | Y | n | n | A | Y | |
| Control | ZZZ | n | A | n | n | n | n | A | n |
Generated by SMTTests/reports/combine-logics-reports.py in the jSMTLIB repository.