From df0b3c86da932ef364f3fbb765eeeeec760442e5 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 20 May 2015 19:09:16 +0200
Subject: [PATCH] update readme with new structure of testcases

---
 README.md | 33 +++++++++++++++++----------------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/README.md b/README.md
index c3cd1502d..afdc26dbf 100644
--- a/README.md
+++ b/README.md
@@ -29,7 +29,7 @@ To build, type this:
 
 Then you can try e.g.
 
-    $ ./leon ./testcases/verification/sas2011-testcases/RedBlackTree.scala
+    $ ./leon ./testcases/verification/datastructures/RedBlackTree.scala
 
 and get something like this:
 
@@ -37,29 +37,30 @@ and get something like this:
   ┌──────────────────────┐
 ╔═╡ Verification Summary ╞════════════════════════════════════════════════════════════════════════╗
 ║ └──────────────────────┘                                                                        ║
-â•‘ add                        postcondition                         82:15   valid    Z3-f    0.066 â•‘
+â•‘ add                        postcondition                         82:15   valid    Z3-f    0.061 â•‘
 â•‘ add                        precond. (call ins(x, t))             81:15   valid    Z3-f    0.004 â•‘
-â•‘ add                        precond. (call makeBlack(ins(x, t)))  81:5    valid    Z3-f    0.021 â•‘
+â•‘ add                        precond. (call makeBlack(ins(x, t)))  81:5    valid    Z3-f    0.017 â•‘
 â•‘ balance                    match exhaustiveness                  90:5    valid    Z3-f    0.006 â•‘
-â•‘ balance                    postcondition                         101:15  valid    Z3-f    0.068 â•‘
-â•‘ blackBalanced              match exhaustiveness                  45:43   valid    Z3-f    0.004 â•‘
-â•‘ blackHeight                match exhaustiveness                  50:40   valid    Z3-f    0.005 â•‘
-â•‘ buggyAdd                   postcondition                         87:15   invalid  Z3-f    2.080 â•‘
+â•‘ balance                    postcondition                         101:15  valid    Z3-f    0.060 â•‘
+â•‘ blackBalanced              match exhaustiveness                  45:43   valid    Z3-f    0.003 â•‘
+â•‘ blackHeight                match exhaustiveness                  50:40   valid    Z3-f    0.004 â•‘
+â•‘ buggyAdd                   postcondition                         87:15   invalid  Z3-f    1.306 â•‘
 â•‘ buggyAdd                   precond. (call ins(x, t))             86:5    invalid  Z3-f    0.027 â•‘
 â•‘ buggyBalance               match exhaustiveness                  104:5   invalid  Z3-f    0.007 â•‘
-â•‘ buggyBalance               postcondition                         115:15  invalid  Z3-f    0.042 â•‘
-â•‘ content                    match exhaustiveness                  17:37   valid    Z3-f    0.027 â•‘
+â•‘ buggyBalance               postcondition                         115:15  invalid  Z3-f    0.029 â•‘
+â•‘ content                    match exhaustiveness                  17:37   valid    Z3-f    0.083 â•‘
+â•‘ flip                       match exhaustiveness                  117:31  valid    Z3-f    0.004 â•‘
 â•‘ ins                        match exhaustiveness                  59:5    valid    Z3-f    0.004 â•‘
-â•‘ ins                        postcondition                         66:15   valid    Z3-f    2.399 â•‘
-â•‘ ins                        precond. (call ins(x, t.left))        62:37   valid    Z3-f    0.013 â•‘
-â•‘ ins                        precond. (call ins(x, t.right))       64:40   valid    Z3-f    0.014 â•‘
-â•‘ makeBlack                  postcondition                         77:14   valid    Z3-f    0.015 â•‘
+â•‘ ins                        postcondition                         66:15   valid    Z3-f    1.385 â•‘
+â•‘ ins                        precond. (call ins(x, t.left))        62:37   valid    Z3-f    0.011 â•‘
+â•‘ ins                        precond. (call ins(x, t.right))       64:40   valid    Z3-f    0.012 â•‘
+â•‘ makeBlack                  postcondition                         77:14   valid    Z3-f    0.013 â•‘
 â•‘ redDescHaveBlackChildren   match exhaustiveness                  40:53   valid    Z3-f    0.004 â•‘
-â•‘ redNodesHaveBlackChildren  match exhaustiveness                  34:54   valid    Z3-f    0.005 â•‘
+â•‘ redNodesHaveBlackChildren  match exhaustiveness                  34:54   valid    Z3-f    0.004 â•‘
 â•‘ size                       match exhaustiveness                  22:33   valid    Z3-f    0.004 â•‘
-â•‘ size                       postcondition                         25:15   valid    Z3-f    0.023 â•‘
+â•‘ size                       postcondition                         25:15   valid    Z3-f    0.048 â•‘
 ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
-â•‘ total: 21     valid: 17     invalid: 4      unknown 0                                     4.838 â•‘
+â•‘ total: 22     valid: 18     invalid: 4      unknown 0                                     3.096 â•‘
 ╚═════════════════════════════════════════════════════════════════════════════════════════════════╝
 </pre>
 
-- 
GitLab