Enable verbose SMT output in debugging mode

[BinderDavid]

The additional output generated by the verbose setting is reasonable in length, in my opinion.
Example:

> gr StdLib/Nat.gr --debug
...
Debug: guardPredicatesStack 
[[(([(n.0 : Nat),(n.1 : Nat)], (n.0 = n.1 + 1) ∧ (n.0 + 1 = 2 * n`0)), StdLib/Nat.gr:75:1)]]

Debug: impossibility 
about to try ([u]n.3 : Nat, [u]n.2 : Nat, [u]n.1 : Nat, [u]n.0 : Nat, [u]n`0 : Nat) . ∃ n.0 : Nat . ∃ n.1 : Nat . (n.0 = n.1 + 1) ∧ (n.0 + 1 = 2 * n`0)

Debug: compiletoSBV 
[u]n.3 : Nat, [u]n.2 : Nat, [u]n.1 : Nat, [u]n.0 : Nat, [u]n`0 : Nat . ∃ n.0 : Nat . ∃ n.1 : Nat . (n.0 = n.1 + 1) ∧ (n.0 + 1 = 2 * n`0)

** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :timeout 10000)
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s4 () Int 0)
[GOOD] (define-fun s9 () Int 1)
[GOOD] (define-fun s13 () Int 2)
[GOOD] ; --- skolem constants ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- preQuantifier assignments ---
[GOOD] ; --- arrayDelayeds ---
[GOOD] ; --- arraySetups ---
[GOOD] ; --- formula ---
[GOOD] (assert (forall ((s0 Int)
                        (s1 Int)
                        (s2 Int)
                        (s3 Int))
       ; --- postQuantifier assignments ---
                   (let ((s5 (>= s0 s4)))
                   (let ((s6 (>= s1 s4)))
                   (let ((s7 (>= s2 s4)))
                   (let ((s8 (>= s3 s4)))
                   (let ((s10 (+ s3 s9)))
                   (let ((s11 (= s2 s10)))
                   (let ((s12 (+ s2 s9)))
                   (let ((s14 (* s0 s13)))
                   (let ((s15 (= s12 s14)))
                   (let ((s16 (and s11 s15)))
                   (let ((s17 (and s8 s16)))
                   (let ((s18 (and s7 s17)))
                   (let ((s19 (and s6 s18)))
                   (let ((s20 (and s5 s19)))
       ; --- delayedEqualities ---
       ; -- finalAssert ---
                   (not s20)))))))))))))))))
[SEND] (check-sat)
[RECV] unsat
*** Solver   : Z3
*** Exit code: ExitSuccess
Debug: compiletoSBV 
True

If this is considered to spammy I can also add a separate flag.