This paper might be worth looking at to help with generating counterexamples from Z3 / Boogie: **Better Counterexamples for Dafny**, TACAS'22 https://assets.amazon.science/51/09/b11373034546962be985d222fcd0/better-counterexamples-for-dafny.pdf
This paper might be worth looking at to help with generating counterexamples from Z3 / Boogie:
Better Counterexamples for Dafny, TACAS'22
https://assets.amazon.science/51/09/b11373034546962be985d222fcd0/better-counterexamples-for-dafny.pdf