From c191f46c6b56e6eb70ce55ef7592b4ee1e311df7 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 6 May 2015 18:07:16 +0200
Subject: [PATCH] Update readme with new preconditions

---
 README.md | 54 +++++++++++++++++++++++++++---------------------------
 1 file changed, 27 insertions(+), 27 deletions(-)

diff --git a/README.md b/README.md
index c35752697..c3cd1502d 100644
--- a/README.md
+++ b/README.md
@@ -34,33 +34,33 @@ Then you can try e.g.
 and get something like this:
 
 <pre>
-    ┌──────────────────────┐
-  ╔═╡ Verification Summary ╞═════════════════════════════════════════════════════════════════════╗
-  ║ └──────────────────────┘                                                                     ║
-  â•‘ add                            postcondition            83:22    valid        Z3-f     0.057 â•‘
-  â•‘ add                            precondition             82:5     valid        Z3-f     0.017 â•‘
-  â•‘ add                            precondition             82:15    valid        Z3-f     0.003 â•‘
-  â•‘ balance                        match exhaustiveness     91:5     valid        Z3-f     0.005 â•‘
-  â•‘ balance                        postcondition            102:22   valid        Z3-f     0.055 â•‘
-  â•‘ blackBalanced                  match exhaustiveness     46:43    valid        Z3-f     0.003 â•‘
-  â•‘ blackHeight                    match exhaustiveness     51:40    valid        Z3-f     0.004 â•‘
-  â•‘ buggyAdd                       postcondition            88:22    invalid      Z3-f     1.162 â•‘
-  â•‘ buggyAdd                       precondition             87:5     invalid      Z3-f     0.027 â•‘
-  â•‘ buggyBalance                   match exhaustiveness     105:5    invalid      Z3-f     0.007 â•‘
-  â•‘ buggyBalance                   postcondition            116:22   invalid      Z3-f     0.017 â•‘
-  â•‘ content                        match exhaustiveness     18:37    valid        Z3-f     0.034 â•‘
-  â•‘ ins                            match exhaustiveness     60:5     valid        Z3-f     0.003 â•‘
-  â•‘ ins                            postcondition            67:22    valid        Z3-f     1.753 â•‘
-  â•‘ ins                            precondition             63:37    valid        Z3-f     0.011 â•‘
-  â•‘ ins                            precondition             65:40    valid        Z3-f     0.012 â•‘
-  â•‘ makeBlack                      postcondition            78:21    valid        Z3-f     0.012 â•‘
-  â•‘ redDescHaveBlackChildren       match exhaustiveness     41:53    valid        Z3-f     0.003 â•‘
-  â•‘ redNodesHaveBlackChildren      match exhaustiveness     35:54    valid        Z3-f     0.004 â•‘
-  â•‘ size                           match exhaustiveness     23:33    valid        Z3-f     0.004 â•‘
-  â•‘ size                           postcondition            26:15    valid        Z3-f     0.043 â•‘
-  ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
-  â•‘ total: 21     valid: 17     invalid: 4      unknown 0                                  3.236 â•‘
-  ╚══════════════════════════════════════════════════════════════════════════════════════════════╝
+  ┌──────────────────────┐
+╔═╡ Verification Summary ╞════════════════════════════════════════════════════════════════════════╗
+║ └──────────────────────┘                                                                        ║
+â•‘ add                        postcondition                         82:15   valid    Z3-f    0.066 â•‘
+â•‘ 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 â•‘
+â•‘ 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 â•‘
+â•‘ 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 â•‘
+â•‘ 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 â•‘
+â•‘ redDescHaveBlackChildren   match exhaustiveness                  40:53   valid    Z3-f    0.004 â•‘
+â•‘ redNodesHaveBlackChildren  match exhaustiveness                  34:54   valid    Z3-f    0.005 â•‘
+â•‘ size                       match exhaustiveness                  22:33   valid    Z3-f    0.004 â•‘
+â•‘ size                       postcondition                         25:15   valid    Z3-f    0.023 â•‘
+╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
+â•‘ total: 21     valid: 17     invalid: 4      unknown 0                                     4.838 â•‘
+╚═════════════════════════════════════════════════════════════════════════════════════════════════╝
 </pre>
 
 Building Leon
-- 
GitLab