## A Formal Proof of a Unix Path Resolution Algorithm

A Path Resolution Algorithm is shown terminating, correct and complete. The design of the formal specification and the implementation of the algorithm is described in the report A Formal Proof of a Unix Path Resolution Algorithm

Auteurs: Claude Marché / Martin Clochard / Ran Chen

Catégories: Inductive predicates

Outils: Why3

Références: CoLiS project / ProofInUse joint laboratory

see also the index (by topic, by tool, by reference, by year)

# A Formal Proof of an Unix Path Resolution Algorithm

## Formalization of File Systems and Path Resolution

```module FileSystem

use import int.Int
use import int.MinMax

use export list.List
use export option.Option

```

### Pathnames

```  type filename
type pathcomponent = Down filename | Up | Here
```

Up denotes ".." and Here denotes "."

```  type path = list pathcomponent

```

### File System

```  type dirnode
type child =
| Absent
| Dir dirnode
constant root : dirnode
function lookup dirnode filename : child
function parent dirnode : dirnode
axiom parent_root: parent root = root
axiom parent_non_root: forall d1 f d2. lookup d1 f = Dir d2 -> parent d2 = d1

```

### Resolution Predicates

```  inductive resolve_to dirnode path dirnode =
| ResolveNil : forall d. resolve_to d Nil d
| ResolveDir : forall d1 fn d2 p d3.
lookup d1 fn = Dir d2 -> resolve_to d2 p d3 -> resolve_to d1 (Cons (Down fn) p) d3
| ResolveAbsLink : forall d1 fn ps pr d2 d3.
lookup d1 fn = AbsLink ps -> resolve_to root ps d2 -> resolve_to d2 pr d3 ->
resolve_to d1 (Cons (Down fn) pr) d3
| ResolveRelLink : forall d1 fn ps pr d2 d3.
lookup d1 fn = RelLink ps -> resolve_to d1 ps d2 -> resolve_to d2 pr d3 ->
resolve_to d1 (Cons (Down fn) pr) d3
| ResolveUp: forall d1 d2 d3 p.
parent d1 = d2 -> resolve_to d2 p d3 -> resolve_to d1 (Cons Up p) d3
| ResolveHere: forall d1 p d2.
resolve_to d1 p d2 -> resolve_to d1 (Cons Here p) d2

inductive resolve_with_height dirnode path (option (dirnode,int)) =
| ResolveHeightAbsent: forall d p. (forall d1. not resolve_to d p d1) ->
resolve_with_height d p None
| ResolveHeightNil : forall d. resolve_with_height d Nil (Some (d,0))
| ResolveHeightDir : forall d1 fn d2 p d3 h.
lookup d1 fn = Dir d2 -> resolve_with_height d2 p (Some(d3,h)) ->
resolve_with_height d1 (Cons (Down fn) p) (Some (d3,h + 1))
| ResolveHeightAbsLink : forall d1 fn ps pr d2 d3 h1 h2.
lookup d1 fn = AbsLink ps -> resolve_with_height root ps (Some (d2,h1)) ->
resolve_with_height d2 pr (Some (d3,h2)) ->
resolve_with_height d1 (Cons (Down fn) pr) (Some (d3, max h1 h2 + 1))
| ResolveHeightRelLink : forall d1 fn ps pr d2 d3 h1 h2.
lookup d1 fn = RelLink ps -> resolve_with_height d1 ps (Some (d2,h1)) ->
resolve_with_height d2 pr (Some (d3,h2)) ->
resolve_with_height d1 (Cons (Down fn) pr) (Some (d3,max h1 h2 + 1))
| ResolveHeightUp : forall d1 d2 d3 p h.
parent d1 = d2 -> resolve_with_height d2 p (Some(d3, h)) ->
resolve_with_height d1 (Cons Up p) (Some (d3,h + 1))
| ResolveHeightHere : forall d1 p d2 h.
resolve_with_height d1 p (Some (d2,h)) ->
resolve_with_height d1 (Cons Here p) (Some (d2,h + 1))

lemma resolve_height_resolve : forall d1 p d2 h.
resolve_with_height d1 p (Some(d2, h)) -> resolve_to d1 p d2

lemma resolve_height_pos : forall d1 p d2 h.
resolve_with_height d1 p (Some (d2,h)) -> h >= 0

lemma resolve_make_height : forall d1 p d2. resolve_to d1 p d2 ->
exists h. resolve_with_height d1 p (Some(d2, h))

end

```

## Conformance with POSIX informal definition

```module POSIX_resolution

use import FileSystem
use import list.Append

lemma resolve_to_append : forall d1 d2 d3 p q.
("induction" resolve_to d1 p d2) ->
resolve_to d2 q d3 ->
resolve_to d1 (p ++ q) d3

lemma resolve_to_cons : forall d1 d2 d3 c p.
resolve_to d1 (Cons c Nil) d2 ->
resolve_to d2 p d3 ->
resolve_to d1 (Cons c p) d3

let lemma resolve_to_decomp (d1 d3:dirnode) (c:pathcomponent) (p2:path)
requires { resolve_to d1 (Cons c p2) d3 }
ensures { exists d2. resolve_to d1 (Cons c Nil) d2 /\ resolve_to d2 p2 d3 }
= ()

let lemma resolve_to_decomposition (p1 p2:path) (d1 d3:dirnode)
requires { resolve_to d1 (p1 ++ p2) d3 }
ensures { exists d2. resolve_to d1 p1 d2 /\ resolve_to d2 p2 d3 }
= ()

inductive resolve_to_POSIX dirnode path dirnode =
| ResolveNilPOSIX : forall d. resolve_to_POSIX d Nil d
| ResolveDirPOSIX : forall d1 fn d2 p d3.
lookup d1 fn = Dir d2 -> resolve_to_POSIX d2 p d3 ->
resolve_to_POSIX d1 (Cons (Down fn) p) d3
| ResolveAbsLinkPOSIX : forall d1 fn ps pr d2.
lookup d1 fn = AbsLink ps -> resolve_to_POSIX root (ps ++ pr) d2 ->
resolve_to_POSIX d1 (Cons (Down fn) pr) d2
| ResolveRelLinkPOSIX : forall d1 fn ps pr d2.
lookup d1 fn = RelLink ps -> resolve_to_POSIX d1 (ps ++ pr) d2 ->
resolve_to_POSIX d1 (Cons (Down fn) pr) d2
| ResolveUpPOSIX: forall d1 d2 d3 p.
parent d1 = d2 -> resolve_to_POSIX d2 p d3 ->
resolve_to_POSIX d1 (Cons Up p) d3
| ResolveHerePOSIX: forall d1 p d2.
resolve_to_POSIX d1 p d2 -> resolve_to_POSIX d1 (Cons Here p) d2

lemma resolve_to_POSIX_append:
forall d1 d2 p1. resolve_to_POSIX d1 p1 d2 ->
forall p2 d3. resolve_to_POSIX d2 p2 d3 ->
resolve_to_POSIX d1 (p1 ++ p2) d3

lemma resolve_to_equivalence:
forall d1 d2 p. resolve_to_POSIX d1 p d2 <-> resolve_to d1 p d2

end

```

## Determinism of Path Resolution

```theory Determinism

use import int.Int
use import FileSystem

lemma resolve_unique : forall d1 p d2.
resolve_to d1 p d2 -> forall d3. resolve_to d1 p d3 -> d2 = d3

lemma resolve_with_height_unique:
forall d p h1. resolve_with_height d p h1 ->
forall h2. resolve_with_height d p h2 -> h1 = h2
by match h1, h2 with
| None, None -> true
| _, None | None, _ -> false
| Some(_,u), Some(_,v) -> u = v end

lemma resolve_with_height_exists :
forall d p. exists h. resolve_with_height d p h

end

```

## Path Resolution Algorithm

```module Resolution

use import int.Int
use import FileSystem
use Determinism

```

obvious technical lemmas, but needed to help provers

```  lemma resolve_height_absLink:
forall d x p r h ps d' h'. resolve_with_height d (Cons (Down x) p) (Some(r, h)) ->
lookup d x = AbsLink ps -> resolve_with_height root ps (Some(d', h')) -> h' <= h

forall d x p r h ps d' h'. resolve_with_height d (Cons (Down x) p) (Some(r, h)) ->
lookup d x = RelLink ps -> resolve_with_height d ps (Some(d', h')) -> h' <= h

use import set.Fset
use import map.Map

type lnk = (dirnode,filename)
axiom alllinks_in : forall d fn ps.
lookup d fn = AbsLink ps \/ lookup d fn = RelLink ps -> mem (d,fn) alllinks

exception Error

let rec aux_resolve (d: dirnode) (p:path) (active:set lnk) : dirnode
requires { subset active alllinks }
requires { forall d1 fn ps d2.
mem (d1, fn) active -> lookup d1 fn = AbsLink ps ->
resolve_to root ps d2 -> exists r. resolve_to d p r}
requires { forall d1 fn ps d2.
mem (d1, fn) active -> lookup d1 fn = RelLink ps ->
resolve_to d1 ps d2 -> exists r. resolve_to d p r}
requires { forall d1 fn ps d2 h1 d' h.
mem (d1,fn) active -> lookup d1 fn = AbsLink ps ->
resolve_with_height root ps (Some(d2, h1)) ->
resolve_with_height d p (Some(d', h)) -> h <= h1 }
requires { forall d1 fn ps d2 h1 d' h.
mem (d1,fn) active -> lookup d1 fn = RelLink ps ->
resolve_with_height d1 ps (Some(d2, h1)) ->
resolve_with_height d p (Some (d',h)) -> h <= h1 }
ensures { resolve_to d p result }
raises { Error -> forall d'. not resolve_to d p d' }
variant { cardinal alllinks - cardinal active, p }
= assert {exists h. resolve_with_height d p h }; (* to help provers *)
match p with
| Nil -> d
| Cons Up pr -> let d' = parent d in aux_resolve d' pr active
| Cons Here pr -> aux_resolve d pr active
| Cons (Down fn) pr ->
match lookup d fn with
| Absent -> raise Error
| Dir d' -> aux_resolve d' pr active
if mem (d,fn) active
then raise Error
else begin
let d' = aux_resolve root ps actadd in
aux_resolve d' pr active
end
if mem (d, fn) active
then raise Error
else begin
let d' = aux_resolve d ps actadd in
aux_resolve d' pr active
end
end
end

let resolve (d: dirnode) (p:path) : dirnode
ensures { resolve_to d p result }
raises { Error -> forall d2. not resolve_to d p d2 }
= aux_resolve d p empty

end
```

# Why3 Proof Results for Project "path_resolution"

## Theory "path_resolution.FileSystem": fully verified in 25.88 s

 Obligations Alt-Ergo (1.01) CVC3 (2.4.1) CVC4 (1.4) Eprover (1.8-001) Z3 (4.4.1) resolve_height_resolve --- --- --- --- --- induction_pr 1. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.01 0.02 0.04 0.02 0.02 2. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.01 0.03 0.04 0.17 0.01 3. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.04 0.06 0.05 6.44 0.02 4. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 1.06 Timeout (10s) 0.06 6.10 0.02 5. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 1.00 Timeout (10s) 0.05 Timeout (10s) 0.02 6. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.03 0.03 0.04 0.17 0.02 7. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.01 0.02 0.04 0.16 0.02 resolve_height_pos --- --- --- --- --- induction_pr 1. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.01 0.02 0.04 0.02 0.01 2. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.01 0.02 0.03 0.16 0.01 3. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.01 0.04 0.03 0.16 0.01 4. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.02 0.03 0.04 0.18 0.04 5. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.01 0.02 0.03 0.18 0.03 6. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.01 0.02 0.03 0.17 0.02 7. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.01 0.02 0.04 0.17 0.02 resolve_make_height --- --- --- --- --- induction_pr 1. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.02 Timeout (10s) 4.98 0.06 Timeout (10s) 2. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.03 Timeout (10s) 0.05 1.26 0.01 3. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. Timeout (10s) Timeout (10s) 0.13 2.55 0.02 4. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. Timeout (10s) Timeout (10s) 0.12 3.57 0.02 5. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.04 Timeout (10s) 0.05 0.17 0.02 6. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.02 0.03 0.05 0.17 0.01

## Theory "path_resolution.POSIX_resolution": fully verified in 24.09 s

 Obligations Alt-Ergo (1.01) CVC3 (2.4.1) CVC4 (1.4) Coq (8.5pl1) Eprover (1.8-001) Z3 (4.4.1) resolve_to_append --- --- --- --- --- --- induction_pr 1. 0.01 0.03 0.05 --- 0.02 0.01 2. Timeout (10s) Timeout (10s) 0.04 --- 0.21 Timeout (10s) 3. Timeout (10s) Timeout (10s) 0.05 --- 0.52 Timeout (10s) 4. Timeout (10s) Timeout (10s) 0.07 --- 0.23 Timeout (10s) 5. Timeout (10s) Timeout (10s) 0.04 --- 0.20 Timeout (10s) 6. 0.13 Timeout (10s) 0.05 --- 0.20 Timeout (10s) resolve_to_cons Timeout (10s) 2.62 0.05 --- 0.22 0.04 VC for resolve_to_decomp --- --- --- --- --- --- induction_pr 1. VC for resolve_to_decomp 0.01 0.02 0.07 --- 0.02 0.02 2. VC for resolve_to_decomp Timeout (10s) Timeout (10s) Timeout (10s) --- 0.26 Timeout (10s) 3. VC for resolve_to_decomp Timeout (10s) Timeout (10s) Timeout (10s) --- 0.67 0.04 4. VC for resolve_to_decomp Timeout (10s) Timeout (10s) Timeout (10s) --- 0.83 0.04 5. VC for resolve_to_decomp Timeout (10s) Timeout (10s) 1.14 --- 0.20 Timeout (10s) 6. VC for resolve_to_decomp 1.20 0.08 0.71 --- 0.19 0.05 VC for resolve_to_decomposition --- --- --- --- --- --- induction_ty_lex 1. VC for resolve_to_decomposition --- --- --- --- --- --- split_goal_wp 1. postcondition 0.15 0.03 0.09 --- 0.16 0.03 2. postcondition Timeout (10s) Timeout (10s) 7.22 1.61 Timeout (10s) Timeout (10s) resolve_to_POSIX_append --- --- --- --- --- --- induction_pr 1. 0.02 0.03 0.05 --- 0.02 0.03 2. Timeout (10s) Timeout (10s) 0.04 --- 0.43 Timeout (10s) 3. Timeout (10s) Timeout (10s) 2.10 --- 0.42 Timeout (10s) 4. Timeout (10s) Timeout (10s) 1.23 --- 0.36 Timeout (10s) 5. Timeout (10s) Timeout (10s) 0.04 --- 0.28 Timeout (10s) 6. Timeout (10s) Timeout (10s) 0.04 --- 0.28 3.14 resolve_to_equivalence --- --- --- --- --- --- split_goal_wp 1. --- --- --- --- --- --- induction_pr 1. 0.02 0.03 0.04 --- 0.02 0.02 2. Timeout (10s) Timeout (10s) 0.04 --- 0.27 Timeout (10s) 3. Timeout (10s) Timeout (10s) 0.06 --- Timeout (10s) Timeout (10s) 4. Timeout (10s) Timeout (10s) 0.08 --- Timeout (10s) Timeout (10s) 5. Timeout (10s) Timeout (10s) 0.07 --- 0.27 Timeout (10s) 6. 0.02 0.04 0.04 --- 0.26 0.03 2. --- --- --- --- --- --- induction_pr 1. 0.02 0.03 0.04 --- 0.03 0.02 2. Timeout (10s) Timeout (10s) 0.04 --- 0.28 Timeout (10s) 3. Timeout (10s) Timeout (10s) 0.05 --- 0.29 Timeout (10s) 4. Timeout (10s) Timeout (10s) 0.05 --- 0.31 Timeout (10s) 5. Timeout (10s) Timeout (10s) 0.05 --- 0.27 Timeout (10s) 6. 0.02 0.04 0.03 --- 0.26 0.03

## Theory "path_resolution.Determinism": fully verified in 34.98 s

 Obligations Alt-Ergo (1.01) CVC3 (2.4.1) CVC4 (1.4) Eprover (1.8-001) Z3 (4.4.1) resolve_unique --- --- --- --- --- induction_pr 1. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 0.03 Timeout (10s) 7.00 0.17 Timeout (10s) 2. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. Timeout (10s) 0.85 Timeout (10s) Timeout (10s) Timeout (10s) 3. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. --- --- --- --- --- inversion_pr 1. 0.01 0.02 0.04 0.02 0.01 2. 0.01 0.02 0.04 0.17 0.02 3. Timeout (10s) 0.78 1.63 0.17 0.07 4. 0.01 0.02 0.03 0.17 0.01 5. 0.01 0.03 0.04 0.06 0.02 6. 0.02 0.06 0.04 0.06 0.02 4. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. --- --- --- --- --- inversion_pr 1. 0.01 0.02 0.04 0.02 0.02 2. 0.01 0.03 0.04 0.18 0.02 3. 0.01 0.02 0.04 0.18 0.02 4. Timeout (10s) 0.06 1.31 0.18 0.06 5. 0.01 0.02 0.04 0.06 0.02 6. 0.01 0.07 0.04 0.06 0.02 5. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 4.08 0.91 6.28 Timeout (10s) Timeout (10s) 6. --- --- --- --- --- simplify_trivial_quantification_in_goal 1. 3.52 0.31 4.09 Timeout (10s) Timeout (10s) resolve_with_height_unique --- --- --- --- --- split_goal_wp 1. 0.03 Timeout (10s) Timeout (10s) Timeout (10s) Timeout (10s) 2. 0.05 Timeout (10s) Timeout (10s) 7.87 Timeout (10s) 3. --- --- --- --- --- induction_pr 1. --- --- --- --- --- inversion_pr 1. 0.02 0.02 0.04 0.02 0.02 2. 0.02 0.02 0.03 0.02 0.02 3. 0.02 0.03 0.04 0.02 0.02 4. 0.02 0.03 0.04 0.02 0.02 5. 0.02 0.03 0.04 0.01 0.02 6. 0.02 0.03 0.04 0.02 0.02 7. 0.02 0.03 0.14 0.02 0.02 2. 0.01 Timeout (10s) Timeout (10s) 0.17 Timeout (10s) 3. --- --- --- --- --- inversion_pr 1. 0.02 0.03 0.05 0.02 0.02 2. 0.02 0.03 0.04 0.02 0.02 3. Timeout (10s) Timeout (10s) 0.05 0.24 Timeout (10s) 4. 0.02 0.03 0.05 0.24 0.02 5. 0.02 0.03 0.05 0.19 0.02 6. 0.02 0.02 0.04 0.18 0.02 7. 0.02 0.08 0.04 0.18 0.02 4. --- --- --- --- --- inversion_pr 1. 0.02 0.03 0.04 0.02 0.02 2. 0.02 0.03 0.05 0.02 0.03 3. 0.02 0.03 0.06 0.19 0.02 4. Timeout (10s) Timeout (10s) 0.12 Timeout (10s) Timeout (10s) 5. 0.02 0.04 0.05 0.18 0.02 6. 0.02 0.03 0.05 0.19 0.02 7. 0.02 0.15 0.05 0.19 0.02 5. --- --- --- --- --- inversion_pr 1. 0.02 0.03 0.05 0.02 0.02 2. 0.02 0.03 0.04 0.02 0.02 3. 0.02 0.03 0.05 0.18 0.02 4. 0.02 0.03 0.06 0.18 0.03 5. Timeout (10s) Timeout (10s) 0.13 Timeout (10s) Timeout (10s) 6. 0.02 0.03 0.05 0.11 0.03 7. 0.02 0.20 0.05 0.19 0.02 6. --- --- --- --- --- inversion_pr 1. 0.02 0.02 0.04 0.02 0.02 2. 0.02 0.02 0.04 0.02 0.02 3. 0.02 0.02 0.05 0.17 0.03 4. 0.02 0.03 0.05 0.18 0.02 5. 0.02 0.03 0.05 0.18 0.02 6. Timeout (10s) Timeout (10s) 0.14 0.20 Timeout (10s) 7. 0.02 0.08 0.04 0.18 0.02 7. --- --- --- --- --- inversion_pr 1. 0.02 0.03 0.04 0.02 0.02 2. 0.02 0.03 0.04 0.01 0.02 3. 0.02 0.08 0.03 0.17 0.02 4. 0.02 0.14 0.05 0.18 0.02 5. 0.02 0.14 0.05 0.18 0.02 6. 0.02 0.09 0.04 0.18 0.03 7. Timeout (10s) Timeout (10s) 0.04 0.21 Timeout (10s) 4. 0.18 Timeout (10s) 0.05 0.18 0.03 resolve_with_height_exists 0.02 Timeout (10s) 0.03 0.17 Timeout (10s)

## Theory "path_resolution.Resolution": fully verified in 91.32 s

 Obligations Alt-Ergo (1.01) CVC3 (2.4.1) CVC4 (1.4) Eprover (1.8-001) Z3 (4.4.1) resolve_height_absLink Timeout (10s) 0.18 Timeout (10s) Timeout (10s) Timeout (10s) resolve_height_relLink Timeout (10s) 0.16 Timeout (10s) Timeout (10s) Timeout (10s) VC for aux_resolve --- --- --- --- --- split_goal_wp 1. assertion 0.05 Timeout (10s) 4.74 0.12 Timeout (10s) 2. postcondition 0.01 0.04 0.06 0.03 0.03 3. variant decrease 0.01 0.04 0.07 0.23 0.03 4. precondition 0.01 0.04 0.06 0.07 0.03 5. precondition 0.23 0.24 Timeout (10s) Timeout (10s) Timeout (10s) 6. precondition 0.21 0.24 Timeout (10s) Timeout (10s) Timeout (10s) 7. precondition Timeout (10s) Timeout (10s) 0.14 Timeout (10s) 0.03 8. precondition Timeout (10s) Timeout (10s) 0.14 Timeout (10s) 0.04 9. postcondition 0.02 0.04 0.07 0.08 0.03 10. exceptional postcondition 0.11 0.11 4.76 Timeout (10s) 2.33 11. variant decrease 0.02 0.04 0.06 0.22 0.04 12. precondition 0.02 0.04 0.05 0.07 0.03 13. precondition 0.19 0.24 Timeout (10s) Timeout (10s) Timeout (10s) 14. precondition 0.19 0.23 Timeout (10s) Timeout (10s) Timeout (10s) 15. precondition 2.45 Timeout (10s) 0.15 Timeout (10s) 0.03 16. precondition 2.16 Timeout (10s) 0.14 Timeout (10s) 0.03 17. postcondition 0.02 0.04 0.07 0.25 0.02 18. exceptional postcondition 0.10 0.11 4.66 Timeout (10s) 2.29 19. exceptional postcondition 0.04 0.08 Timeout (10s) Timeout (10s) 1.71 20. variant decrease 0.02 0.04 0.06 0.23 0.04 21. precondition 0.02 0.03 0.05 0.07 0.02 22. precondition 0.15 0.28 Timeout (10s) Timeout (10s) Timeout (10s) 23. precondition 0.13 0.27 Timeout (10s) Timeout (10s) Timeout (10s) 24. precondition Timeout (10s) Timeout (10s) 0.12 Timeout (10s) 0.03 25. precondition Timeout (10s) Timeout (10s) 0.13 Timeout (10s) 0.04 26. postcondition 0.02 0.04 0.06 0.26 0.03 27. exceptional postcondition 0.05 0.12 7.92 Timeout (10s) Timeout (10s) 28. exceptional postcondition 4.50 Timeout (10s) Timeout (10s) Timeout (10s) Timeout (10s) 29. variant decrease 0.03 0.05 0.07 Timeout (10s) 0.03 30. precondition Timeout (10s) 0.13 0.07 Timeout (10s) 0.02 31. precondition 0.55 0.34 Timeout (10s) Timeout (10s) Timeout (10s) 32. precondition 0.45 0.37 Timeout (10s) Timeout (10s) Timeout (10s) 33. precondition 8.17 Timeout (10s) Timeout (10s) Timeout (10s) Timeout (10s) 34. precondition 3.90 Timeout (10s) Timeout (10s) Timeout (10s) Timeout (10s) 35. variant decrease 0.03 0.05 0.07 0.24 Timeout (10s) 36. precondition 0.02 0.04 0.05 0.08 0.02 37. precondition Timeout (10s) 1.65 Timeout (10s) Timeout (10s) Timeout (10s) 38. precondition Timeout (10s) 1.81 Timeout (10s) Timeout (10s) Timeout (10s) 39. precondition Timeout (10s) Timeout (10s) 2.37 Timeout (10s) 4.80 40. precondition Timeout (10s) Timeout (10s) 2.35 Timeout (10s) 1.46 41. postcondition 0.03 Timeout (10s) 0.07 Timeout (10s) 0.03 42. exceptional postcondition Timeout (10s) 0.96 Timeout (10s) Timeout (10s) Timeout (10s) 43. exceptional postcondition 0.05 0.24 Timeout (10s) Timeout (10s) Timeout (10s) 44. exceptional postcondition 1.62 Timeout (10s) Timeout (10s) Timeout (10s) 6.25 45. variant decrease 0.03 0.04 0.07 Timeout (10s) 0.03 46. precondition 0.03 Timeout (10s) 4.79 Timeout (10s) Timeout (10s) 47. precondition 0.48 0.31 Timeout (10s) Timeout (10s) Timeout (10s) 48. precondition 0.47 0.31 6.07 Timeout (10s) Timeout (10s) 49. precondition 4.27 Timeout (10s) Timeout (10s) Timeout (10s) Timeout (10s) 50. precondition 7.45 Timeout (10s) Timeout (10s) Timeout (10s) Timeout (10s) 51. variant decrease 0.03 0.04 0.08 0.25 0.30 52. precondition 0.02 0.04 0.06 0.07 0.03 53. precondition Timeout (10s) 1.92 Timeout (10s) Timeout (10s) Timeout (10s) 54. precondition Timeout (10s) 2.89 Timeout (10s) Timeout (10s) Timeout (10s) 55. precondition Timeout (10s) Timeout (10s) 2.04 Timeout (10s) 3.09 56. precondition Timeout (10s) Timeout (10s) 1.73 Timeout (10s) 0.47 57. postcondition 0.03 Timeout (10s) 0.08 0.29 0.02 58. exceptional postcondition Timeout (10s) 0.94 Timeout (10s) Timeout (10s) Timeout (10s) 59. exceptional postcondition 0.16 0.23 Timeout (10s) Timeout (10s) Timeout (10s) VC for resolve --- --- --- --- --- split_goal_wp 1. precondition 0.03 0.03 0.06 0.21 0.03 2. precondition 0.02 0.04 0.05 0.02 0.02 3. precondition 0.01 0.04 0.06 0.02 0.02 4. precondition 0.03 0.04 0.05 0.02 0.03 5. precondition 0.03 0.03 0.06 0.03 0.03 6. postcondition 0.03 0.03 0.05 0.03 0.01 7. exceptional postcondition 0.03 0.04 0.07 0.03 0.00