This is Leon 0.2.0

To build it, you will need, for example, the following:
  * Java Runtime Environment, from Oracle, e.g. Version 7 Update 5 
    (to run xsbt and scala)
  * Scala, from Typesafe, e.g. version 2.9.1
  * xsbt, e.g. version 0.11.3: download sbt-launch.jar, run it with java -jar
    (to built Leon)
  * a recent GLIBC3 or later, works with e.g. apt-get
    (for Z3)
  * GNU Multiprecision library, e.g. gmp3, works with e.g. apt-get
    (for Z3)

To build, type this:

xsbt clean   
xsbt package # takes a while
xsbt script

Then you can try e.g.

./run-demo demo/RedBlackTree.scala

and get something like this:

[ Info  ] . ┌─────────┐
          ╔═╡ Summary ╞═══════════════════════════════════════════════════════════════════════╗
          ║ └─────────┘                                                                       ║
          ║ add                       postcond.           valid               Z3-f+t    0.314 ║
          ║ add                       precond.    (82,14) valid               Z3-f+t    0.020 ║
          ║ add                       precond.    (82,18) valid               Z3-f+t    0.005 ║
          ║ balance                   postcond.           valid               Z3-f+t    0.409 ║
          ║ balance                   match.      (91,19) valid               Z3-f+t    0.034 ║
          ║ blackHeight               match.      (51,39) valid               Z3-f+t    0.004 ║
          ║ buggyAdd                  postcond.           invalid             Z3-f+t    4.084 ║
          ║ buggyAdd                  precond.     (87,8) invalid             Z3-f+t    0.111 ║
          ║ buggyBalance              postcond.           invalid             Z3-f+t    0.055 ║
          ║ buggyBalance              match.     (105,19) invalid             Z3-f+t    0.007 ║
          ║ ins                       postcond.           valid               Z3-f+t    6.577 ║
          ║ ins                       precond.    (63,40) valid               Z3-f+t    0.021 ║
          ║ ins                       precond.    (65,43) valid               Z3-f+t    0.005 ║
          ║ makeBlack                 postcond.           valid               Z3-f+t    0.007 ║
          ║ redNodesHaveBlackChildren match.      (35,56) valid               Z3-f+t    0.003 ║
          ║ size                      postcond.           valid               Z3-f+t    0.012 ║
          ╚═══════════════════════════════════════════════════════════════════════════════════╝

Additional information:
=======================
Sample output of 
  ldd lib-bin/lib3.so
is:
	linux-gate.so.1 =>  (0x00b13000)
	libgmp.so.3 => /usr/lib/libgmp.so.3 (0x00110000)
	libstdc++.so.6 => /usr/lib/i386-linux-gnu/libstdc++.so.6 (0x0016f000)
	libm.so.6 => /lib/i386-linux-gnu/libm.so.6 (0x0025a000)
	libgcc_s.so.1 => /lib/i386-linux-gnu/libgcc_s.so.1 (0x00709000)
	libc.so.6 => /lib/i386-linux-gnu/libc.so.6 (0x004d9000)
	/lib/ld-linux.so.2 (0x002ab000)