title: dafny corresponding SMT queries
body: <p>I'm trying to inspect a simple looping program that <strong>finds the maximal element in an integer array</strong>. Here is the permalink <a href="https://rise4fun.com/Dafny/hrITU" rel="nofollow noreferrer">here</a>. Everything works fine, but I'm really interested in
  the resulting SMT file, so I extracted it using:</p>
  
  <pre><code>$ dafny /compile:3 /proverLog:./mySMT.smt myCode.dfy
  </code></pre>
  
  <p>Then ran with <code>z3</code> as follows:</p>
  
  <pre><code>$ z3 ./mySMT.smt
  </code></pre>
  
  <p>I got 3 <code>unsat</code> responses and I was wondering <strong>what are the corresponding 3 queries</strong>?
  I looked at the <code>*.smt</code> file and found 11K of machine-generated SMT.
  Any tips on deciphering the smt file? thanks!</p>