Possible usage of Nim & Z3 for embedded?

[moerm]

Btw, there have been found north of 1000 bugs in Z3 and other solvers are 
unlikely to be much better.

Maybe we need a solver written in Ada, F star or at least in Nim ...