Tried to use MiniZinc to write a model checker [1] for c programs a while back [2]. Essentially checking the equivalence of c functions that use only bit operations. It basically translates the programs into minizinc, then attempts to derive a case where the same input results in differing output. Was a fun way to experiment using the constraint solver for a practical application, though unfortunately didn't work as well on larger more complicated functions.
1) https://en.wikipedia.org/wiki/Model_checking
2) https://github.com/dbunker/ArchStatMzn