寻找SMT Z3 usecases(类似DbC)和开源替代Z3的实例?

I have got interested in and looking for practical examples of SMT Z3 usage (like DbC) with code and open source alternatives to this tool. So, in fact, I am interested in similar Z3 formal solving tools, but:I have got interested in and looking for practi