search

SRI-CSL / sally

A model checker for infinite-state systems.
http://sri-csl.github.io/sally/
GNU General Public License v2.0
69 stars 12 forks source link

Missing `floor` function? #56

Closed yav closed 5 years ago

yav commented 5 years ago

It looks like sally's to_int function rounds towards 0. It would be nice to also have a floor function, which always rounds down, to match the functionality of jkind. For example see:

https://github.com/agacek/jkind/blob/master/testing/cast.lus

yav commented 5 years ago

Never mind, I was confused---the SMTLIB standard says that to_int rounds towards negative infinity and this is what sally does.

So I am going to close this for now.