Date: 10-Jul-2012, 15:08:30
Host: DFCS-MCARLISLE
Non-option args: 
    spark_dns_main
Option args: 
    -fuse-concls   \
    -decls=c:\spark\2011\bin\../share/spark/prelude.fdl   \
    -unique-working-files   \
    -rules=c:\spark\2011\bin\../share/spark/prelude.rul   \
    -rules=c:\spark\2011\bin\../share/spark/divmod.rul   \
    -elim-enums   \
    -ground-eval-exp   \
    -abstract-exp   \
    -abstract-divmod   \
    -utick   \
    -gtick   \
    -longtick   \
    -echo-final-stats   \
    -csv-reports-include-unit-kind   \
    -level=warning   \
    -bit-type   \
    -bit-type-bool-eq-to-iff   \
    -refine-types   \
    -refine-int-subrange-type   \
    -abstract-arrays-records-late   \
    -elim-array-constructors   \
    -add-array-select-box-update-axioms   \
    -abstract-array-box-updates   \
    -add-array-select-update-axioms   \
    -abstract-array-select-updates   \
    -abstract-array-types   \
    -abstract-record-types   \
    -abstract-bit-ops   \
    -abstract-bit-valued-eqs   \
    -abstract-bit-valued-int-le   \
    -elim-bit-type-and-consts   \
    -abstract-reals   \
    -lift-quants   \
    -strip-quantifier-patterns   \
    -elim-type-aliases   \
    -interface-mode=smtlib   \
    -refine-bit-type-as-int-subtype   \
    -refine-bit-eq-equiv   \
    -elim-record-constructors   \
    -add-record-select-update-axioms   \
    -abstract-record-selects-updates   \
    -logic=AUFNIRA   \
    -report=spark_dns_main   \
    -prover-command=c:\spark\2011\bin\alt-ergo.exe -steps  5000   \
    -siv   \



Total ERROR   messages: 0
Total WARNING messages: 0

Summary Stats: 
    true:    0  ( nan%)
unproven:    0  ( nan%)    [timeout:    0  ( nan%) ]
   error:    0  ( nan%)
   total:    0

Time: 0.05s  (u: 0.02s, s: 0.03s, cu: 0.00s, cs: 0.00s,  0.0% ch, 66.7% sys)