Very interesting, thanks a lot for writing this article! However, I was expecting a bit more details on how Z3 helped here, I’ve only read a few articles about Z3 before so I was interested in a new use case but I didn’t realize until the end where the Z3 bits were :)
EDIT: just another thing, your gist is commented in French, not a problem for me, but it might easier for other people to have comments in English given that the article is in English ;)
Yep, you’re right, the article was a bit messy. I originally started writing it months ago, and forgot most of the details since then. The trick is to use Z3’s BitVecs, since we’re not working with numbers but with bits. At line 137 I’m converting the ints into doubles, into bits. There probably is a way to speed up the solving with node.js v10 but I didn’t find any working Z3 method for it.
I also updated the gist so the comments are now in english, thanks for noticing.
Related article from a few years ago