apalache-mc / apalache

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

produce true on distinct for less than 2 elements #3005

Closed konnov closed 1 month ago

konnov commented 2 months ago

Closes #2964. Simply translate distinst into true, when we have less than two subexpressions. It's only relevant for replaying SMT logs in CVC5, but it was sufficiently annoying for me to fix it.