search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
243 stars 34 forks source link

uses of distinct with ABC #281

Closed LeventErkok closed 7 years ago

LeventErkok commented 7 years ago

Currently ABC has a bug that causes it to ignore > 2 arguments if present to distinct.

https://bitbucket.org/alanmi/abc/issues/68/smt-interface-distinct-is-an-n-ary

Hopefully Alan will fix this soon. If not, we might want to recognize this case and if the solver is ABC, we either want to translate to pairwise inequalities ourself, or reject. Otherwise ABC simply does the wrong thing, causing soundness issues.

LeventErkok commented 7 years ago

This is now fixed in ABC!