search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
439 stars 40 forks source link

Do not produce distinct on singleton #2964

Closed konnov closed 1 month ago

konnov commented 2 months ago

This is a minor annoyance. Apalache produces (distinct ..) even for singletons. This is what cvc5 complains about. We should simply fix it, so it would be possible to repay the SMT log with cvc5.