Skip to content

Instantly share code, notes, and snippets.

@NatKarmios

NatKarmios/file.log

Created February 28, 2024 04:44
Show Gist options
  • Save NatKarmios/96cbf6cab030291ef54c640116296ead to your computer and use it in GitHub Desktop.
Save NatKarmios/96cbf6cab030291ef54c640116296ead to your computer and use it in GitHub Desktop.
Download ZIP
Gillian verification example log
Raw
file.log
*** Phase ***
*** Phase ***
*** MESSAGE: Adding procedure: i__add.
*** MESSAGE: Adding procedure: i__lt.
*** MESSAGE: Adding procedure: i__minus.
*** MESSAGE: Adding procedure: i__geq.
*** MESSAGE: Adding procedure: i__ptr_add.
*** MESSAGE: Adding procedure: i__leq.
*** MESSAGE: Adding procedure: i__gt.
*** MESSAGE: Adding predicate: i__pred_gt.
*** MESSAGE: Adding predicate: i__pred_lt.
*** MESSAGE: Adding predicate: i__pred_leq.
*** MESSAGE: Adding predicate: i__pred_add.
*** MESSAGE: Adding predicate: i__pred_minus.
*** MESSAGE: Adding predicate: i__pred_geq.
*** Phase ***
*** MESSAGE: Adding predicate: i__pred_cell.
*** MESSAGE: Adding predicate: freed.
Program as parsed:
@internal
pred i__pred_geq(+el, +er, out) : types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) * (out == (not (#offsetl i< #offsetr))),
types(el : Int, er : Int) * (out == (not (el i< er)));
@internal
pred i__pred_add(+el, +er, out) : types(el : List, er : Int) *
(el == {{ #loc, #offset }}) * (out == {{ #loc, (#offset i+ er) }}),
types(er : List, el : Int) * (er == {{ #loc, #offset }}) *
(out == {{ #loc, (#offset i+ el) }}), types(er : Int, el : Int) *
(out == (er i+ el));
@internal
pred i__pred_minus(+el, +er, out) : types(el : List, er : Int) *
(el == {{ #loc, #offset }}) * (out == {{ #loc, (#offset i- er) }}),
types(er : Int, el : Int) * (out == (el i- er));
@internal
pred i__pred_leq(+el, +er, out) : types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) * (out == (#offsetl i<= #offsetr)),
types(el : Int, er : Int) * (out == (el i<= er));
@internal
pred i__pred_lt(+el, +er, out) : types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) * (out == (#offsetl i< #offsetr)),
types(el : Int, er : Int) * (out == (el i< er));
pred list(+x, alpha : List) : (x == null) * (alpha == {{ }}),
<cell>(#wisl__0, #wisl__1; #v) * <cell>(#wisl__0, (#wisl__1 i+ 1i); #z) *
types(#wisl__0 : Obj, #wisl__1 : Int) * (x == {{ #wisl__0, #wisl__1 }}) *
list(#z, #beta) * (alpha == l+ ({{ #v }}, #beta));
@internal
pred freed(ptr : List) : (ptr == {{ #l, 0i }}) * types(#l : Obj) *
<freed>(#l; );
@internal
pred i__pred_gt(+el, +er, out) : types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) * (out == (not (#offsetl i<= #offsetr))),
types(el : Int, er : Int) * (out == (not (el i<= er)));
@internal
pred i__pred_cell(+ptr : List, value) : (ptr == {{ #loc, #offset }}) *
<cell>(#loc, #offset; value);
@internal
proc i__lt(el, er) {
goto [((typeOf el) = List)] 1 10;
locl := l-nth(el, 0i);
locr := l-nth(er, 0i);
goto [(locr = locr)] 6 4;
message := "Cannot compare these two values";
fail [message](locl, locr);
offsetl := l-nth(el, 1i);
offsetr := l-nth(er, 1i);
ret := (offsetl i< offsetr);
return;
ret := (el i< er);
return
};
@internal
proc i__add(el, er) {
goto [(((typeOf el) = List) and ((typeOf er) = Int))] 1 3;
ret := "i__ptr_add"(el, er);
return;
goto [(((typeOf er) = List) and ((typeOf el) = Int))] 4 6;
ret := "i__ptr_add"(er, el);
return;
goto [(((typeOf el) = Int) and ((typeOf el) = Int))] 7 9;
ret := (el i+ er);
return;
err_msg := "Addition: Incorrect Types";
fail [err_msg](el, er)
};
@internal
proc i__minus(el, er) {
goto [((typeOf el) = List)] 1 4;
mer := (i- er);
ret := "i__ptr_add"(el, mer);
goto 5;
ret := (el i- er);
return
};
@internal
proc i__geq(el, er) {
goto [((typeOf el) = List)] 1 10;
locl := l-nth(el, 0i);
locr := l-nth(er, 0i);
goto [(locr = locr)] 6 4;
message := "Cannot compare these two values";
fail [message](locl, locr);
offsetl := l-nth(el, 1i);
offsetr := l-nth(er, 1i);
ret := (not (offsetl i< offsetr));
return;
ret := (not (el i< er));
return
};
@internal
proc i__ptr_add(ptr, add_offset) {
loc := l-nth(ptr, 0i);
offset := l-nth(ptr, 1i);
ret := {{ loc, (offset i+ add_offset) }};
return
};
spec llen(x)
[[ (x == #x) * list(#x, #alpha) ]]
[[ list(#x, #alpha) * (ret == (l-len #alpha)) ]]
normal
proc llen(x) {
goto [(x = null)] 1 3;
n := 1i;
goto 11;
gvar0 := "i__add"(x, 1i);
goto [((typeOf gvar0) = List)] 6 5;
fail [InvalidPointer]();
gvar1 := [getcell](l-nth(gvar0, 0i), l-nth(gvar0, 1i));
t := l-nth(gvar1, 2i);
n := "llen"(t);
gvar2 := "i__add"(n, 1i);
n := gvar2;
skip;
ret := n;
return
};
@internal
proc i__leq(el, er) {
goto [((typeOf el) = List)] 1 10;
locl := l-nth(el, 0i);
locr := l-nth(er, 0i);
goto [(locr = locr)] 6 4;
message := "Cannot compare pointers from different blocks";
fail [message](locl, locr);
offsetl := l-nth(el, 1i);
offsetr := l-nth(er, 1i);
ret := (offsetl i<= offsetr);
return;
ret := (el i<= er);
return
};
@internal
proc i__gt(el, er) {
goto [((typeOf el) = List)] 1 10;
locl := l-nth(el, 0i);
locr := l-nth(er, 0i);
goto [(locr = locr)] 6 4;
message := "Cannot compare these two values";
fail [message](locl, locr);
offsetl := l-nth(el, 1.);
offsetr := l-nth(er, 1.);
ret := (not (offsetl i<= offsetr));
return;
ret := (not (el i<= er));
return
};
*** Phase ***
Unfold order: i__pred_geq, i__pred_minus, i__pred_add, i__pred_leq,
i__pred_lt, freed, i__pred_gt, i__pred_cell,
list
Unfolding predicate: i__pred_geq
PFS/Gamma simplification:
With matching: No
PFS:
(#locr == #locl)
(#__out == (not (#offsetl i< #offsetr)))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (not (#offsetl i< #offsetr)))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #locl, #offsetl }})
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (not (#offsetl i< #offsetr)))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #locl, #offsetl }})
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (not (#offsetl i< #offsetr)))
Gamma:
(#__el: List)
(#__er: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__out == (not (#__el i< #__er)))
Gamma:
(#__el: Int)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#__er: Int)
Definitions' has a length of 2
Pruning.
Predicate i__pred_geq has 2 definitions before pruning.
Predicate i__pred_geq left with 2 definitions after pruning.
Done pruning.
Unfolding predicate: i__pred_minus
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #loc, #offset }})
(#__out == {{ #loc, (#offset i- #__er) }})
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__er: Int)
(#offset: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #loc, #offset }})
(#__out == {{ #loc, (#offset i- #__er) }})
Gamma:
(#__el: List)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__er: Int)
(#offset: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__out == (#__el i- #__er))
Gamma:
(#__el: Int)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#__er: Int)
Definitions' has a length of 2
Pruning.
Predicate i__pred_minus has 2 definitions before pruning.
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #loc, #offset }})
(#__out == {{ #loc, ((-1i i* #__er) i+ #offset) }})
Gamma:
(#__el: List)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__er: Int)
(#offset: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__out == (#__el i+ (-1i i* #__er)))
Gamma:
(#__el: Int)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#__er: Int)
Predicate i__pred_minus left with 2 definitions after pruning.
Done pruning.
Unfolding predicate: i__pred_add
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #loc, #offset }})
(#__out == {{ #loc, (#offset i+ #__er) }})
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__er: Int)
(#offset: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #loc, #offset }})
(#__out == {{ #loc, (#offset i+ #__er) }})
Gamma:
(#__el: List)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__er: Int)
(#offset: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__er == {{ #loc, #offset }})
(#__out == {{ #loc, (#offset i+ #__el) }})
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#offset: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__er == {{ #loc, #offset }})
(#__out == {{ #loc, (#offset i+ #__el) }})
Gamma:
(#__el: Int)
(#__er: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#offset: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__out == (#__er i+ #__el))
Gamma:
(#__el: Int)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#__er: Int)
Definitions' has a length of 3
Pruning.
Predicate i__pred_add has 3 definitions before pruning.
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #loc, #offset }})
(#__out == {{ #loc, (#__er i+ #offset) }})
Gamma:
(#__el: List)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__er: Int)
(#offset: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__er == {{ #loc, #offset }})
(#__out == {{ #loc, (#__el i+ #offset) }})
Gamma:
(#__el: Int)
(#__er: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#offset: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__out == (#__el i+ #__er))
Gamma:
(#__el: Int)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#__er: Int)
Predicate i__pred_add left with 3 definitions after pruning.
Done pruning.
Unfolding predicate: i__pred_leq
PFS/Gamma simplification:
With matching: No
PFS:
(#locr == #locl)
(#__out == (#offsetl i<= #offsetr))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (#offsetl i<= #offsetr))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #locl, #offsetl }})
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (#offsetl i<= #offsetr))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #locl, #offsetl }})
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (#offsetl i<= #offsetr))
Gamma:
(#__el: List)
(#__er: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__out == (#__el i<= #__er))
Gamma:
(#__el: Int)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#__er: Int)
Definitions' has a length of 2
Pruning.
Predicate i__pred_leq has 2 definitions before pruning.
Predicate i__pred_leq left with 2 definitions after pruning.
Done pruning.
Unfolding predicate: i__pred_lt
PFS/Gamma simplification:
With matching: No
PFS:
(#locr == #locl)
(#__out == (#offsetl i< #offsetr))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (#offsetl i< #offsetr))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #locl, #offsetl }})
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (#offsetl i< #offsetr))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #locl, #offsetl }})
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (#offsetl i< #offsetr))
Gamma:
(#__el: List)
(#__er: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__out == (#__el i< #__er))
Gamma:
(#__el: Int)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#__er: Int)
Definitions' has a length of 2
Pruning.
Predicate i__pred_lt has 2 definitions before pruning.
Predicate i__pred_lt left with 2 definitions after pruning.
Done pruning.
Unfolding predicate: freed
PFS/Gamma simplification:
With matching: No
PFS:
Gamma:
(#l: Obj)
PFS/Gamma simplification completed:
PFS:
Gamma:
(#l: Obj)
PFS/Gamma simplification:
With matching: No
PFS:
(#__ptr == {{ #l, 0i }})
Gamma:
(#l: Obj)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#l: Obj)
PFS/Gamma simplification:
With matching: No
PFS:
(#__ptr == {{ #l, 0i }})
Gamma:
(#__ptr: List)
(#l: Obj)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#l: Obj)
Definitions' has a length of 1
Pruning.
Predicate freed has 1 definitions before pruning.
Predicate freed left with 1 definitions after pruning.
Done pruning.
Unfolding predicate: i__pred_gt
PFS/Gamma simplification:
With matching: No
PFS:
(#locr == #locl)
(#__out == (not (#offsetl i<= #offsetr)))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (not (#offsetl i<= #offsetr)))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #locl, #offsetl }})
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (not (#offsetl i<= #offsetr)))
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__el == {{ #locl, #offsetl }})
(#__er == {{ #locr, #offsetr }})
(#locr == #locl)
(#__out == (not (#offsetl i<= #offsetr)))
Gamma:
(#__el: List)
(#__er: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#offsetl: Int)
(#offsetr: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__out == (not (#__el i<= #__er)))
Gamma:
(#__el: Int)
(#__er: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#__el: Int)
(#__er: Int)
Definitions' has a length of 2
Pruning.
Predicate i__pred_gt has 2 definitions before pruning.
Predicate i__pred_gt left with 2 definitions after pruning.
Done pruning.
Unfolding predicate: i__pred_cell
PFS/Gamma simplification:
With matching: No
PFS:
(#__ptr == {{ #loc, #offset }})
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
PFS/Gamma simplification:
With matching: No
PFS:
(#__ptr == {{ #loc, #offset }})
Gamma:
(#__ptr: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
Definitions' has a length of 1
Pruning.
Predicate i__pred_cell has 1 definitions before pruning.
Predicate i__pred_cell left with 1 definitions after pruning.
Done pruning.
Unfolding predicate: list
PFS/Gamma simplification:
With matching: No
PFS:
(#__x == null)
(#__alpha == {{ }})
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
PFS/Gamma simplification:
With matching: No
PFS:
(#__x == null)
(#__alpha == {{ }})
Gamma:
(#__alpha: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
PFS/Gamma simplification:
With matching: No
PFS:
Gamma:
(#beta: List)
PFS/Gamma simplification completed:
PFS:
Gamma:
(#beta: List)
PFS/Gamma simplification:
With matching: No
PFS:
(#__alpha == l+ ({{ #v }}, #beta))
Gamma:
(#beta: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len #beta))
Gamma:
(#beta: List)
PFS/Gamma simplification:
With matching: No
PFS:
Gamma:
PFS/Gamma simplification completed:
PFS:
Gamma:
PFS/Gamma simplification:
With matching: No
PFS:
Gamma:
(#wisl__0: Obj)
(#wisl__1: Int)
PFS/Gamma simplification completed:
PFS:
Gamma:
(#wisl__0: Obj)
(#wisl__1: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__x == {{ #wisl__0, #wisl__1 }})
Gamma:
(#wisl__0: Obj)
(#wisl__1: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
(#wisl__0: Obj)
(#wisl__1: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__x == {{ #wisl__0, #wisl__1 }})
(#__alpha == l+ ({{ #v }}, #beta))
Gamma:
(#beta: List)
(#wisl__0: Obj)
(#wisl__1: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len #beta))
Gamma:
(#beta: List)
(#wisl__0: Obj)
(#wisl__1: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#__x == {{ #wisl__0, #wisl__1 }})
(#__alpha == l+ ({{ #v }}, #beta))
Gamma:
(#__alpha: List)
(#beta: List)
(#wisl__0: Obj)
(#wisl__1: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len #beta))
Gamma:
(#beta: List)
(#wisl__0: Obj)
(#wisl__1: Int)
Definitions' has a length of 2
Pruning.
Predicate list has 2 definitions before pruning.
PFS/Gamma simplification:
With matching: No
PFS:
(#__x == null)
(#__alpha == {{ }})
Gamma:
(#__alpha: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
Predicate list left with 2 definitions after pruning.
Done pruning.
PFS/Gamma simplification:
With matching: No
PFS:
Gamma:
(#alpha: List)
PFS/Gamma simplification completed:
PFS:
Gamma:
(#alpha: List)
PFS/Gamma simplification:
With matching: No
PFS:
(#__x == #x)
Gamma:
(#alpha: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len #alpha))
Gamma:
(#alpha: List)
Pre admissibility: llen
PFS/Gamma simplification:
With matching: No
PFS:
(#__ret == (l-len #alpha))
Gamma:
(#alpha: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len #alpha))
Gamma:
(#alpha: List)
Post admissibility: llen
Program after logic preprocessing:
@internal
pred i__pred_geq(+el, +er, out) : types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) * (out == (not (#offsetl i< #offsetr))),
types(el : Int, er : Int) * (out == (not (el i< er)));
@internal
pred i__pred_minus(+el, +er, out) : types(el : List, er : Int) *
(el == {{ #loc, #offset }}) *
(out == {{ #loc, ((-1i i* er) i+ #offset) }}), types(el : Int, er : Int) *
(out == (el i+ (-1i i* er)));
@internal
pred i__pred_add(+el, +er, out) : types(el : List, er : Int) *
(el == {{ #loc, #offset }}) * (out == {{ #loc, (er i+ #offset) }}),
types(el : Int, er : List) * (er == {{ #loc, #offset }}) *
(out == {{ #loc, (el i+ #offset) }}), types(el : Int, er : Int) *
(out == (el i+ er));
@internal
pred i__pred_leq(+el, +er, out) : types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) * (out == (#offsetl i<= #offsetr)),
types(el : Int, er : Int) * (out == (el i<= er));
@internal
pred i__pred_lt(+el, +er, out) : types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) * (out == (#offsetl i< #offsetr)),
types(el : Int, er : Int) * (out == (el i< er));
@internal
pred freed(ptr : List) : types(ptr : List, #l : Obj) *
(ptr == {{ #l, 0i }}) * <freed>(#l; );
facts: ((typeOf ptr) == List);
pred list(+x, alpha : List) : types(alpha : List) * (x == null) *
(alpha == {{ }}),
types(alpha : List, #beta : List, #wisl__0 : Obj, #wisl__1 : Int) *
<cell>(#wisl__0, #wisl__1; #v) * <cell>(#wisl__0, (1i i+ #wisl__1); #z) *
(x == {{ #wisl__0, #wisl__1 }}) * list(#z, #beta) *
(alpha == l+ ({{ #v }}, #beta));
facts: ((typeOf alpha) == List);
@internal
pred i__pred_gt(+el, +er, out) : types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) * (out == (not (#offsetl i<= #offsetr))),
types(el : Int, er : Int) * (out == (not (el i<= er)));
@internal
pred i__pred_cell(+ptr : List, value) : types(ptr : List) *
(ptr == {{ #loc, #offset }}) * <cell>(#loc, #offset; value);
facts: ((typeOf ptr) == List);
@internal
proc i__lt(el, er) {
goto [((typeOf el) = List)] 1 10;
locl := l-nth(el, 0i);
locr := l-nth(er, 0i);
goto [(locr = locr)] 6 4;
message := "Cannot compare these two values";
fail [message](locl, locr);
offsetl := l-nth(el, 1i);
offsetr := l-nth(er, 1i);
ret := (offsetl i< offsetr);
return;
ret := (el i< er);
return
};
@internal
proc i__add(el, er) {
goto [(((typeOf el) = List) and ((typeOf er) = Int))] 1 3;
ret := "i__ptr_add"(el, er);
return;
goto [(((typeOf er) = List) and ((typeOf el) = Int))] 4 6;
ret := "i__ptr_add"(er, el);
return;
goto [(((typeOf el) = Int) and ((typeOf el) = Int))] 7 9;
ret := (el i+ er);
return;
err_msg := "Addition: Incorrect Types";
fail [err_msg](el, er)
};
@internal
proc i__minus(el, er) {
goto [((typeOf el) = List)] 1 4;
mer := (i- er);
ret := "i__ptr_add"(el, mer);
goto 5;
ret := (el i- er);
return
};
@internal
proc i__geq(el, er) {
goto [((typeOf el) = List)] 1 10;
locl := l-nth(el, 0i);
locr := l-nth(er, 0i);
goto [(locr = locr)] 6 4;
message := "Cannot compare these two values";
fail [message](locl, locr);
offsetl := l-nth(el, 1i);
offsetr := l-nth(er, 1i);
ret := (not (offsetl i< offsetr));
return;
ret := (not (el i< er));
return
};
@internal
proc i__ptr_add(ptr, add_offset) {
loc := l-nth(ptr, 0i);
offset := l-nth(ptr, 1i);
ret := {{ loc, (offset i+ add_offset) }};
return
};
spec llen(x)
[[ (x == #x) * types(#alpha : List) * list(#x, #alpha) ]]
[[ types(#alpha : List) * list(#x, #alpha) * (ret == (l-len #alpha)) ]]
normal
proc llen(x) {
goto [(x = null)] 1 3;
n := 1i;
goto 11;
gvar0 := "i__add"(x, 1i);
goto [((typeOf gvar0) = List)] 6 5;
fail [InvalidPointer]();
gvar1 := [getcell](l-nth(gvar0, 0i), l-nth(gvar0, 1i));
t := l-nth(gvar1, 2i);
n := "llen"(t);
gvar2 := "i__add"(n, 1i);
n := gvar2;
skip;
ret := n;
return
};
@internal
proc i__leq(el, er) {
goto [((typeOf el) = List)] 1 10;
locl := l-nth(el, 0i);
locr := l-nth(er, 0i);
goto [(locr = locr)] 6 4;
message := "Cannot compare pointers from different blocks";
fail [message](locl, locr);
offsetl := l-nth(el, 1i);
offsetr := l-nth(er, 1i);
ret := (offsetl i<= offsetr);
return;
ret := (el i<= er);
return
};
@internal
proc i__gt(el, er) {
goto [((typeOf el) = List)] 1 10;
locl := l-nth(el, 0i);
locr := l-nth(er, 0i);
goto [(locr = locr)] 6 4;
message := "Cannot compare these two values";
fail [message](locl, locr);
offsetl := l-nth(el, 1.);
offsetr := l-nth(er, 1.);
ret := (not (offsetl i<= offsetr));
return;
ret := (not (el i<= er));
return
};
*** Phase ***
Attempting to create MP of predicate i__pred_cell
Known matchables: {PVar ptr}
Existentials: {}
Entering s-init on: types(ptr : List) * (ptr == {{ #loc, #offset }}) *
<cell>(#loc, #offset; value)
KB: {PVar ptr}
KNOWN: {PVar ptr}.
CUR MP:
[]
TO VISIT: types(PVar ptr : List)
(PVar ptr == {{ LVar #loc, LVar #offset }})
<cell>(LVar #loc, LVar #offset; PVar value)
KNOWN: {PVar ptr}.
CUR MP:
[types(ptr : List), ]
TO VISIT: (PVar ptr == {{ LVar #loc, LVar #offset }})
<cell>(LVar #loc, LVar #offset; PVar value)
IO Equality: (ptr == {{ #loc, #offset }})
Ins: [{PVar ptr, LVar #loc, LVar #offset}]
KB: {PVar ptr}
Known left: true Known right: false
List of expressions: [(#loc, l-nth(ptr, 0i)); (#offset, l-nth(ptr, 1i))]
Result: [({PVar ptr}, (#loc, l-nth(ptr, 0i)); (#offset, l-nth(ptr, 1i)))]
KNOWN: {PVar ptr, LVar #loc, LVar #offset}.
CUR MP:
[(ptr == {{ #loc, #offset }}), (#loc, l-nth(ptr, 0i)); (#offset, l-nth(ptr, 1i));
types(ptr : List), ]
TO VISIT: <cell>(LVar #loc, LVar #offset; PVar value)
Ins_and_outs_from_lists:
Ins: [#loc; #offset]
Outs: [value]
Calculated ins: [{LVar #loc, LVar #offset}]
KNOWN: {PVar ptr, PVar value, LVar #loc, LVar #offset}.
CUR MP:
[<cell>(#loc, #offset; value), (value, 0);
(ptr == {{ #loc, #offset }}), (#loc, l-nth(ptr, 0i)); (#offset, l-nth(ptr, 1i));
types(ptr : List), ]
TO VISIT:
Successfully created MP.
Successfully created MP of predicate i__pred_cell:
┬À types(ptr : List),
┬À (ptr == {{ #loc, #offset }}), (#loc, l-nth(ptr, 0i)); (#offset, l-nth(ptr, 1i))
┬À <cell>(#loc, #offset; value), (value, 0)
===FINISHED=== POST: None
Attempting to create MP of predicate i__pred_gt
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) *
(out == (not (#offsetl i<= #offsetr)))
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : List)
types(PVar er : List)
(PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (not (#offsetl i<= #offsetr)))
(LVar #locr == LVar #locl)
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : List), ]
TO VISIT: types(PVar er : List)
(PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (not (#offsetl i<= #offsetr)))
(LVar #locr == LVar #locl)
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : List), ; types(el : List), ]
TO VISIT: (PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (not (#offsetl i<= #offsetr)))
(LVar #locr == LVar #locl)
IO Equality: (el == {{ #locl, #offsetl }})
Ins: [{PVar el, LVar #locl, LVar #offsetl}]
KB: {PVar el, PVar er}
Known left: true Known right: false
List of expressions: [(#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i))]
Result: [({PVar el}, (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i)))]
KNOWN: {PVar el, PVar er, LVar #locl, LVar #offsetl}.
CUR MP:
[(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (not (#offsetl i<= #offsetr)))
(LVar #locr == LVar #locl)
IO Equality: (er == {{ #locr, #offsetr }})
Ins: [{PVar er, LVar #locr, LVar #offsetr}]
KB: {PVar el, PVar er, LVar #locl, LVar #offsetl}
Known left: true Known right: false
List of expressions: [(#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i))]
Result: [({PVar er}, (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i)))]
KNOWN: {PVar el, PVar er, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (PVar out == (not (#offsetl i<= #offsetr)))
(LVar #locr == LVar #locl)
IO Equality: (out == (not (#offsetl i<= #offsetr)))
Ins: [{PVar out, LVar #offsetl, LVar #offsetr}]
KB: {PVar el, PVar er, LVar #locl, LVar #locr, LVar #offsetl, LVar #offsetr}
Known left: false Known right: true
Result: [({LVar #offsetl, LVar #offsetr},
(out, (not (#offsetl i<= #offsetr))))]
KNOWN: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(out == (not (#offsetl i<= #offsetr))), (out, (not (#offsetl i<= #offsetr)));
(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (LVar #locr == LVar #locl)
IO Equality: (#locr == #locl)
Ins: [{LVar #locl, LVar #locr}]
KB: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}
Known left: true Known right: true
KNOWN: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(#locr == #locl), ;
(out == (not (#offsetl i<= #offsetr))), (out, (not (#offsetl i<= #offsetr)));
(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT:
Successfully created MP.
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : Int, er : Int) *
(out == (not (el i<= er)))
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : Int)
types(PVar er : Int)
(PVar out == (not (el i<= er)))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : Int), ]
TO VISIT: types(PVar er : Int)
(PVar out == (not (el i<= er)))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : Int), ; types(el : Int), ]
TO VISIT: (PVar out == (not (el i<= er)))
IO Equality: (out == (not (el i<= er)))
Ins: [{PVar el, PVar er, PVar out}]
KB: {PVar el, PVar er}
Known left: false Known right: true
Result: [({PVar el, PVar er}, (out, (not (el i<= er))))]
KNOWN: {PVar el, PVar er, PVar out}.
CUR MP:
[(out == (not (el i<= er))), (out, (not (el i<= er))); types(er : Int), ;
types(el : Int), ]
TO VISIT:
Successfully created MP.
Successfully created MP of predicate i__pred_gt:
CHOICE
Ôö£ÔöÇÔöÇ ┬À types(el : List),
Ôöé ┬À types(er : List),
Ôöé ┬À (el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i))
Ôöé ┬À (er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i))
Ôöé ┬À (out == (not (#offsetl i<= #offsetr))), (out, (not (#offsetl i<= #offsetr)))
Ôöé ┬À (#locr == #locl),
Ôöé ===FINISHED=== POST: None
Ôöé
ÔööÔöÇÔöÇ┬À types(el : Int),
┬À types(er : Int),
┬À (out == (not (el i<= er))), (out, (not (el i<= er)))
===FINISHED=== POST: None
Attempting to create MP of predicate list
Known matchables: {PVar x}
Existentials: {}
Entering s-init on: types(alpha : List) * (x == null) *
(alpha == {{ }})
KB: {PVar x}
KNOWN: {PVar x}.
CUR MP:
[]
TO VISIT: types(PVar alpha : List)
(PVar alpha == {{ }})
(PVar x == Lit null)
IO Equality: (alpha == {{ }})
Ins: [{PVar alpha}]
KB: {PVar x}
Known left: false Known right: true
Result: [({}, (alpha, {{ }}))]
KNOWN: {PVar alpha, PVar x}.
CUR MP:
[(alpha == {{ }}), (alpha, {{ }})]
TO VISIT: types(PVar alpha : List)
(PVar x == Lit null)
KNOWN: {PVar alpha, PVar x}.
CUR MP:
[types(alpha : List), ; (alpha == {{ }}), (alpha, {{ }})]
TO VISIT: (PVar x == Lit null)
IO Equality: (x == null)
Ins: [{PVar x}]
KB: {PVar alpha, PVar x}
Known left: true Known right: true
KNOWN: {PVar alpha, PVar x}.
CUR MP:
[(x == null), ; types(alpha : List), ; (alpha == {{ }}), (alpha, {{ }})]
TO VISIT:
Successfully created MP.
Known matchables: {PVar x}
Existentials: {}
Entering s-init on: types(alpha : List, #beta : List, #wisl__0 : Obj,
#wisl__1 : Int) * <cell>(#wisl__0, #wisl__1; #v) *
<cell>(#wisl__0, (1i i+ #wisl__1); #z) * (x == {{ #wisl__0, #wisl__1 }}) *
list(#z, #beta) *
(alpha == l+ ({{ #v }}, #beta))
KB: {PVar x}
KNOWN: {PVar x}.
CUR MP:
[]
TO VISIT: types(PVar alpha : List)
types(LVar #beta : List)
types(LVar #wisl__0 : Obj)
types(LVar #wisl__1 : Int)
(PVar alpha == (NOp l+ ({{ #v }}, #beta)))
(PVar x == {{ LVar #wisl__0, LVar #wisl__1 }})
<cell>(LVar #wisl__0, LVar #wisl__1; LVar #v)
<cell>(LVar #wisl__0, (Lit 1i i+ LVar #wisl__1); LVar #z)
list(LVar #z, LVar #beta)
IO Equality: (alpha == l+ ({{ #v }}, #beta))
Ins: [{PVar alpha, LVar #beta, LVar #v}]
KB: {PVar x}
Known left: false Known right: false
IO Equality: (x == {{ #wisl__0, #wisl__1 }})
Ins: [{PVar x, LVar #wisl__0, LVar #wisl__1}]
KB: {PVar x}
Known left: true Known right: false
List of expressions: [(#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))]
Result: [({PVar x}, (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i)))]
KNOWN: {PVar x, LVar #wisl__0, LVar #wisl__1}.
CUR MP:
[(x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))]
TO VISIT: types(PVar alpha : List)
types(LVar #beta : List)
types(LVar #wisl__0 : Obj)
types(LVar #wisl__1 : Int)
(PVar alpha == (NOp l+ ({{ #v }}, #beta)))
<cell>(LVar #wisl__0, LVar #wisl__1; LVar #v)
<cell>(LVar #wisl__0, (Lit 1i i+ LVar #wisl__1); LVar #z)
list(LVar #z, LVar #beta)
KNOWN: {PVar x, LVar #wisl__0, LVar #wisl__1}.
CUR MP:
[types(#wisl__0 : Obj), ;
(x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))]
TO VISIT: types(PVar alpha : List)
types(LVar #beta : List)
types(LVar #wisl__1 : Int)
(PVar alpha == (NOp l+ ({{ #v }}, #beta)))
<cell>(LVar #wisl__0, LVar #wisl__1; LVar #v)
<cell>(LVar #wisl__0, (Lit 1i i+ LVar #wisl__1); LVar #z)
list(LVar #z, LVar #beta)
KNOWN: {PVar x, LVar #wisl__0, LVar #wisl__1}.
CUR MP:
[types(#wisl__1 : Int), ; types(#wisl__0 : Obj), ;
(x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))]
TO VISIT: types(PVar alpha : List)
types(LVar #beta : List)
(PVar alpha == (NOp l+ ({{ #v }}, #beta)))
<cell>(LVar #wisl__0, LVar #wisl__1; LVar #v)
<cell>(LVar #wisl__0, (Lit 1i i+ LVar #wisl__1); LVar #z)
list(LVar #z, LVar #beta)
IO Equality: (alpha == l+ ({{ #v }}, #beta))
Ins: [{PVar alpha, LVar #beta, LVar #v}]
KB: {PVar x, LVar #wisl__0, LVar #wisl__1}
Known left: false Known right: false
Ins_and_outs_from_lists:
Ins: [#wisl__0; #wisl__1]
Outs: [#v]
Calculated ins: [{LVar #wisl__0, LVar #wisl__1}]
KNOWN: {PVar x, LVar #v, LVar #wisl__0, LVar #wisl__1}.
CUR MP:
[<cell>(#wisl__0, #wisl__1; #v), (#v, 0); types(#wisl__1 : Int), ;
types(#wisl__0 : Obj), ;
(x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))]
TO VISIT: types(PVar alpha : List)
types(LVar #beta : List)
(PVar alpha == (NOp l+ ({{ #v }}, #beta)))
<cell>(LVar #wisl__0, (Lit 1i i+ LVar #wisl__1); LVar #z)
list(LVar #z, LVar #beta)
IO Equality: (alpha == l+ ({{ #v }}, #beta))
Ins: [{PVar alpha, LVar #beta, LVar #v}]
KB: {PVar x, LVar #v, LVar #wisl__0, LVar #wisl__1}
Known left: false Known right: false
Ins_and_outs_from_lists:
Ins: [#wisl__0; (1i i+ #wisl__1)]
Outs: [#z]
Calculated ins: [{LVar #wisl__0, LVar #wisl__1}]
KNOWN: {PVar x, LVar #v, LVar #wisl__0, LVar #wisl__1, LVar #z}.
CUR MP:
[<cell>(#wisl__0, (1i i+ #wisl__1); #z), (#z, 0);
<cell>(#wisl__0, #wisl__1; #v), (#v, 0); types(#wisl__1 : Int), ;
types(#wisl__0 : Obj), ;
(x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))]
TO VISIT: types(PVar alpha : List)
types(LVar #beta : List)
(PVar alpha == (NOp l+ ({{ #v }}, #beta)))
list(LVar #z, LVar #beta)
IO Equality: (alpha == l+ ({{ #v }}, #beta))
Ins: [{PVar alpha, LVar #beta, LVar #v}]
KB: {PVar x, LVar #v, LVar #wisl__0, LVar #wisl__1, LVar #z}
Known left: false Known right: false
Ins_and_outs_from_lists:
Ins: [#z]
Outs: [#beta]
Calculated ins: [{LVar #z}]
KNOWN: {PVar x, LVar #beta, LVar #v, LVar #wisl__0, LVar #wisl__1, LVar #z}.
CUR MP:
[list(#z, #beta), (#beta, 0);
<cell>(#wisl__0, (1i i+ #wisl__1); #z), (#z, 0);
<cell>(#wisl__0, #wisl__1; #v), (#v, 0); types(#wisl__1 : Int), ;
types(#wisl__0 : Obj), ;
(x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))]
TO VISIT: types(PVar alpha : List)
types(LVar #beta : List)
(PVar alpha == (NOp l+ ({{ #v }}, #beta)))
KNOWN: {PVar x, LVar #beta, LVar #v, LVar #wisl__0, LVar #wisl__1, LVar #z}.
CUR MP:
[types(#beta : List), ; list(#z, #beta), (#beta, 0);
<cell>(#wisl__0, (1i i+ #wisl__1); #z), (#z, 0);
<cell>(#wisl__0, #wisl__1; #v), (#v, 0); types(#wisl__1 : Int), ;
types(#wisl__0 : Obj), ;
(x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))]
TO VISIT: types(PVar alpha : List)
(PVar alpha == (NOp l+ ({{ #v }}, #beta)))
IO Equality: (alpha == l+ ({{ #v }}, #beta))
Ins: [{PVar alpha, LVar #beta, LVar #v}]
KB: {PVar x, LVar #beta, LVar #v, LVar #wisl__0, LVar #wisl__1, LVar #z}
Known left: false Known right: true
Result: [({LVar #beta, LVar #v}, (alpha, l+ ({{ #v }}, #beta)))]
KNOWN: {PVar alpha, PVar x, LVar #beta, LVar #v, LVar #wisl__0,
LVar #wisl__1, LVar #z}.
CUR MP:
[(alpha == l+ ({{ #v }}, #beta)), (alpha, l+ ({{ #v }}, #beta));
types(#beta : List), ; list(#z, #beta), (#beta, 0);
<cell>(#wisl__0, (1i i+ #wisl__1); #z), (#z, 0);
<cell>(#wisl__0, #wisl__1; #v), (#v, 0); types(#wisl__1 : Int), ;
types(#wisl__0 : Obj), ;
(x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))]
TO VISIT: types(PVar alpha : List)
KNOWN: {PVar alpha, PVar x, LVar #beta, LVar #v, LVar #wisl__0,
LVar #wisl__1, LVar #z}.
CUR MP:
[types(alpha : List), ;
(alpha == l+ ({{ #v }}, #beta)), (alpha, l+ ({{ #v }}, #beta));
types(#beta : List), ; list(#z, #beta), (#beta, 0);
<cell>(#wisl__0, (1i i+ #wisl__1); #z), (#z, 0);
<cell>(#wisl__0, #wisl__1; #v), (#v, 0); types(#wisl__1 : Int), ;
types(#wisl__0 : Obj), ;
(x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))]
TO VISIT:
Successfully created MP.
Successfully created MP of predicate list:
CHOICE
Ôö£ÔöÇÔöÇ ┬À (alpha == {{ }}), (alpha, {{ }})
Ôöé ┬À types(alpha : List),
Ôöé ┬À (x == null),
Ôöé ===FINISHED=== POST: None
Ôöé
ÔööÔöÇÔöÇ┬À (x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))
┬À types(#wisl__0 : Obj),
┬À types(#wisl__1 : Int),
┬À <cell>(#wisl__0, #wisl__1; #v), (#v, 0)
┬À <cell>(#wisl__0, (1i i+ #wisl__1); #z), (#z, 0)
┬À list(#z, #beta), (#beta, 0)
┬À types(#beta : List),
┬À (alpha == l+ ({{ #v }}, #beta)), (alpha, l+ ({{ #v }}, #beta))
┬À types(alpha : List),
===FINISHED=== POST: None
Attempting to create MP of predicate freed
Known matchables: {PVar ptr}
Existentials: {}
Entering s-init on: types(ptr : List, #l : Obj) * (ptr == {{ #l, 0i }}) *
<freed>(#l; )
KB: {PVar ptr}
KNOWN: {PVar ptr}.
CUR MP:
[]
TO VISIT: types(PVar ptr : List)
types(LVar #l : Obj)
(PVar ptr == {{ LVar #l, Lit 0i }})
<freed>(LVar #l; )
KNOWN: {PVar ptr}.
CUR MP:
[types(ptr : List), ]
TO VISIT: types(LVar #l : Obj)
(PVar ptr == {{ LVar #l, Lit 0i }})
<freed>(LVar #l; )
IO Equality: (ptr == {{ #l, 0i }})
Ins: [{PVar ptr, LVar #l}]
KB: {PVar ptr}
Known left: true Known right: false
List of expressions: [(#l, l-nth(ptr, 0i)); (0i, l-nth(ptr, 1i))]
Result: [({PVar ptr}, (#l, l-nth(ptr, 0i)))]
KNOWN: {PVar ptr, LVar #l}.
CUR MP:
[(ptr == {{ #l, 0i }}), (#l, l-nth(ptr, 0i)); types(ptr : List), ]
TO VISIT: types(LVar #l : Obj)
<freed>(LVar #l; )
KNOWN: {PVar ptr, LVar #l}.
CUR MP:
[types(#l : Obj), ; (ptr == {{ #l, 0i }}), (#l, l-nth(ptr, 0i));
types(ptr : List), ]
TO VISIT: <freed>(LVar #l; )
Ins_and_outs_from_lists:
Ins: [#l]
Outs: []
Calculated ins: [{LVar #l}]
KNOWN: {PVar ptr, LVar #l}.
CUR MP:
[<freed>(#l; ), ; types(#l : Obj), ;
(ptr == {{ #l, 0i }}), (#l, l-nth(ptr, 0i)); types(ptr : List), ]
TO VISIT:
Successfully created MP.
Successfully created MP of predicate freed:
┬À types(ptr : List),
┬À (ptr == {{ #l, 0i }}), (#l, l-nth(ptr, 0i))
┬À types(#l : Obj),
┬À <freed>(#l; ),
===FINISHED=== POST: None
Attempting to create MP of predicate i__pred_lt
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) *
(out == (#offsetl i< #offsetr))
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : List)
types(PVar er : List)
(PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (LVar #offsetl i< LVar #offsetr))
(LVar #locr == LVar #locl)
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : List), ]
TO VISIT: types(PVar er : List)
(PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (LVar #offsetl i< LVar #offsetr))
(LVar #locr == LVar #locl)
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : List), ; types(el : List), ]
TO VISIT: (PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (LVar #offsetl i< LVar #offsetr))
(LVar #locr == LVar #locl)
IO Equality: (el == {{ #locl, #offsetl }})
Ins: [{PVar el, LVar #locl, LVar #offsetl}]
KB: {PVar el, PVar er}
Known left: true Known right: false
List of expressions: [(#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i))]
Result: [({PVar el}, (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i)))]
KNOWN: {PVar el, PVar er, LVar #locl, LVar #offsetl}.
CUR MP:
[(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (LVar #offsetl i< LVar #offsetr))
(LVar #locr == LVar #locl)
IO Equality: (er == {{ #locr, #offsetr }})
Ins: [{PVar er, LVar #locr, LVar #offsetr}]
KB: {PVar el, PVar er, LVar #locl, LVar #offsetl}
Known left: true Known right: false
List of expressions: [(#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i))]
Result: [({PVar er}, (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i)))]
KNOWN: {PVar el, PVar er, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (PVar out == (LVar #offsetl i< LVar #offsetr))
(LVar #locr == LVar #locl)
IO Equality: (out == (#offsetl i< #offsetr))
Ins: [{PVar out, LVar #offsetl, LVar #offsetr}]
KB: {PVar el, PVar er, LVar #locl, LVar #locr, LVar #offsetl, LVar #offsetr}
Known left: false Known right: true
Result: [({LVar #offsetl, LVar #offsetr}, (out, (#offsetl i< #offsetr)))]
KNOWN: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(out == (#offsetl i< #offsetr)), (out, (#offsetl i< #offsetr));
(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (LVar #locr == LVar #locl)
IO Equality: (#locr == #locl)
Ins: [{LVar #locl, LVar #locr}]
KB: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}
Known left: true Known right: true
KNOWN: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(#locr == #locl), ;
(out == (#offsetl i< #offsetr)), (out, (#offsetl i< #offsetr));
(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT:
Successfully created MP.
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : Int, er : Int) *
(out == (el i< er))
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : Int)
types(PVar er : Int)
(PVar out == (PVar el i< PVar er))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : Int), ]
TO VISIT: types(PVar er : Int)
(PVar out == (PVar el i< PVar er))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : Int), ; types(el : Int), ]
TO VISIT: (PVar out == (PVar el i< PVar er))
IO Equality: (out == (el i< er))
Ins: [{PVar el, PVar er, PVar out}]
KB: {PVar el, PVar er}
Known left: false Known right: true
Result: [({PVar el, PVar er}, (out, (el i< er)))]
KNOWN: {PVar el, PVar er, PVar out}.
CUR MP:
[(out == (el i< er)), (out, (el i< er)); types(er : Int), ;
types(el : Int), ]
TO VISIT:
Successfully created MP.
Successfully created MP of predicate i__pred_lt:
CHOICE
Ôö£ÔöÇÔöÇ ┬À types(el : List),
Ôöé ┬À types(er : List),
Ôöé ┬À (el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i))
Ôöé ┬À (er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i))
Ôöé ┬À (out == (#offsetl i< #offsetr)), (out, (#offsetl i< #offsetr))
Ôöé ┬À (#locr == #locl),
Ôöé ===FINISHED=== POST: None
Ôöé
ÔööÔöÇÔöÇ┬À types(el : Int),
┬À types(er : Int),
┬À (out == (el i< er)), (out, (el i< er))
===FINISHED=== POST: None
Attempting to create MP of predicate i__pred_leq
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) *
(out == (#offsetl i<= #offsetr))
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : List)
types(PVar er : List)
(PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (LVar #offsetl i<= LVar #offsetr))
(LVar #locr == LVar #locl)
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : List), ]
TO VISIT: types(PVar er : List)
(PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (LVar #offsetl i<= LVar #offsetr))
(LVar #locr == LVar #locl)
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : List), ; types(el : List), ]
TO VISIT: (PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (LVar #offsetl i<= LVar #offsetr))
(LVar #locr == LVar #locl)
IO Equality: (el == {{ #locl, #offsetl }})
Ins: [{PVar el, LVar #locl, LVar #offsetl}]
KB: {PVar el, PVar er}
Known left: true Known right: false
List of expressions: [(#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i))]
Result: [({PVar el}, (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i)))]
KNOWN: {PVar el, PVar er, LVar #locl, LVar #offsetl}.
CUR MP:
[(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (LVar #offsetl i<= LVar #offsetr))
(LVar #locr == LVar #locl)
IO Equality: (er == {{ #locr, #offsetr }})
Ins: [{PVar er, LVar #locr, LVar #offsetr}]
KB: {PVar el, PVar er, LVar #locl, LVar #offsetl}
Known left: true Known right: false
List of expressions: [(#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i))]
Result: [({PVar er}, (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i)))]
KNOWN: {PVar el, PVar er, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (PVar out == (LVar #offsetl i<= LVar #offsetr))
(LVar #locr == LVar #locl)
IO Equality: (out == (#offsetl i<= #offsetr))
Ins: [{PVar out, LVar #offsetl, LVar #offsetr}]
KB: {PVar el, PVar er, LVar #locl, LVar #locr, LVar #offsetl, LVar #offsetr}
Known left: false Known right: true
Result: [({LVar #offsetl, LVar #offsetr}, (out, (#offsetl i<= #offsetr)))]
KNOWN: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(out == (#offsetl i<= #offsetr)), (out, (#offsetl i<= #offsetr));
(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (LVar #locr == LVar #locl)
IO Equality: (#locr == #locl)
Ins: [{LVar #locl, LVar #locr}]
KB: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}
Known left: true Known right: true
KNOWN: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(#locr == #locl), ;
(out == (#offsetl i<= #offsetr)), (out, (#offsetl i<= #offsetr));
(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT:
Successfully created MP.
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : Int, er : Int) *
(out == (el i<= er))
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : Int)
types(PVar er : Int)
(PVar out == (PVar el i<= PVar er))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : Int), ]
TO VISIT: types(PVar er : Int)
(PVar out == (PVar el i<= PVar er))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : Int), ; types(el : Int), ]
TO VISIT: (PVar out == (PVar el i<= PVar er))
IO Equality: (out == (el i<= er))
Ins: [{PVar el, PVar er, PVar out}]
KB: {PVar el, PVar er}
Known left: false Known right: true
Result: [({PVar el, PVar er}, (out, (el i<= er)))]
KNOWN: {PVar el, PVar er, PVar out}.
CUR MP:
[(out == (el i<= er)), (out, (el i<= er)); types(er : Int), ;
types(el : Int), ]
TO VISIT:
Successfully created MP.
Successfully created MP of predicate i__pred_leq:
CHOICE
Ôö£ÔöÇÔöÇ ┬À types(el : List),
Ôöé ┬À types(er : List),
Ôöé ┬À (el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i))
Ôöé ┬À (er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i))
Ôöé ┬À (out == (#offsetl i<= #offsetr)), (out, (#offsetl i<= #offsetr))
Ôöé ┬À (#locr == #locl),
Ôöé ===FINISHED=== POST: None
Ôöé
ÔööÔöÇÔöÇ┬À types(el : Int),
┬À types(er : Int),
┬À (out == (el i<= er)), (out, (el i<= er))
===FINISHED=== POST: None
Attempting to create MP of predicate i__pred_add
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : List, er : Int) *
(el == {{ #loc, #offset }}) *
(out == {{ #loc, (er i+ #offset) }})
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : List)
types(PVar er : Int)
(PVar el == {{ LVar #loc, LVar #offset }})
(PVar out == {{ LVar #loc, (PVar er i+ LVar #offset) }})
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : List), ]
TO VISIT: types(PVar er : Int)
(PVar el == {{ LVar #loc, LVar #offset }})
(PVar out == {{ LVar #loc, (PVar er i+ LVar #offset) }})
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : Int), ; types(el : List), ]
TO VISIT: (PVar el == {{ LVar #loc, LVar #offset }})
(PVar out == {{ LVar #loc, (PVar er i+ LVar #offset) }})
IO Equality: (el == {{ #loc, #offset }})
Ins: [{PVar el, LVar #loc, LVar #offset}]
KB: {PVar el, PVar er}
Known left: true Known right: false
List of expressions: [(#loc, l-nth(el, 0i)); (#offset, l-nth(el, 1i))]
Result: [({PVar el}, (#loc, l-nth(el, 0i)); (#offset, l-nth(el, 1i)))]
KNOWN: {PVar el, PVar er, LVar #loc, LVar #offset}.
CUR MP:
[(el == {{ #loc, #offset }}), (#loc, l-nth(el, 0i)); (#offset, l-nth(el, 1i));
types(er : Int), ; types(el : List), ]
TO VISIT: (PVar out == {{ LVar #loc, (PVar er i+ LVar #offset) }})
IO Equality: (out == {{ #loc, (er i+ #offset) }})
Ins: [{PVar er, PVar out, LVar #loc, LVar #offset}]
KB: {PVar el, PVar er, LVar #loc, LVar #offset}
Known left: false Known right: true
Result: [({PVar er, LVar #loc, LVar #offset},
(out, {{ #loc, (er i+ #offset) }}))]
KNOWN: {PVar el, PVar er, PVar out, LVar #loc, LVar #offset}.
CUR MP:
[(out == {{ #loc, (er i+ #offset) }}), (out, {{ #loc, (er i+ #offset) }});
(el == {{ #loc, #offset }}), (#loc, l-nth(el, 0i)); (#offset, l-nth(el, 1i));
types(er : Int), ; types(el : List), ]
TO VISIT:
Successfully created MP.
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : Int, er : List) *
(er == {{ #loc, #offset }}) *
(out == {{ #loc, (el i+ #offset) }})
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : Int)
types(PVar er : List)
(PVar er == {{ LVar #loc, LVar #offset }})
(PVar out == {{ LVar #loc, (PVar el i+ LVar #offset) }})
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : Int), ]
TO VISIT: types(PVar er : List)
(PVar er == {{ LVar #loc, LVar #offset }})
(PVar out == {{ LVar #loc, (PVar el i+ LVar #offset) }})
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : List), ; types(el : Int), ]
TO VISIT: (PVar er == {{ LVar #loc, LVar #offset }})
(PVar out == {{ LVar #loc, (PVar el i+ LVar #offset) }})
IO Equality: (er == {{ #loc, #offset }})
Ins: [{PVar er, LVar #loc, LVar #offset}]
KB: {PVar el, PVar er}
Known left: true Known right: false
List of expressions: [(#loc, l-nth(er, 0i)); (#offset, l-nth(er, 1i))]
Result: [({PVar er}, (#loc, l-nth(er, 0i)); (#offset, l-nth(er, 1i)))]
KNOWN: {PVar el, PVar er, LVar #loc, LVar #offset}.
CUR MP:
[(er == {{ #loc, #offset }}), (#loc, l-nth(er, 0i)); (#offset, l-nth(er, 1i));
types(er : List), ; types(el : Int), ]
TO VISIT: (PVar out == {{ LVar #loc, (PVar el i+ LVar #offset) }})
IO Equality: (out == {{ #loc, (el i+ #offset) }})
Ins: [{PVar el, PVar out, LVar #loc, LVar #offset}]
KB: {PVar el, PVar er, LVar #loc, LVar #offset}
Known left: false Known right: true
Result: [({PVar el, LVar #loc, LVar #offset},
(out, {{ #loc, (el i+ #offset) }}))]
KNOWN: {PVar el, PVar er, PVar out, LVar #loc, LVar #offset}.
CUR MP:
[(out == {{ #loc, (el i+ #offset) }}), (out, {{ #loc, (el i+ #offset) }});
(er == {{ #loc, #offset }}), (#loc, l-nth(er, 0i)); (#offset, l-nth(er, 1i));
types(er : List), ; types(el : Int), ]
TO VISIT:
Successfully created MP.
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : Int, er : Int) *
(out == (el i+ er))
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : Int)
types(PVar er : Int)
(PVar out == (PVar el i+ PVar er))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : Int), ]
TO VISIT: types(PVar er : Int)
(PVar out == (PVar el i+ PVar er))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : Int), ; types(el : Int), ]
TO VISIT: (PVar out == (PVar el i+ PVar er))
IO Equality: (out == (el i+ er))
Ins: [{PVar el, PVar er, PVar out}]
KB: {PVar el, PVar er}
Known left: false Known right: true
Result: [({PVar el, PVar er}, (out, (el i+ er)))]
KNOWN: {PVar el, PVar er, PVar out}.
CUR MP:
[(out == (el i+ er)), (out, (el i+ er)); types(er : Int), ;
types(el : Int), ]
TO VISIT:
Successfully created MP.
Successfully created MP of predicate i__pred_add:
CHOICE
Ôö£ÔöÇÔöÇ ┬À types(el : List),
Ôöé ┬À types(er : Int),
Ôöé ┬À (el == {{ #loc, #offset }}), (#loc, l-nth(el, 0i)); (#offset, l-nth(el, 1i))
Ôöé ┬À (out == {{ #loc, (er i+ #offset) }}), (out, {{ #loc,
(er i+ #offset) }})
Ôöé ===FINISHED=== POST: None
Ôöé
ÔööÔöÇÔöÇ┬À types(el : Int),
CHOICE
Ôö£ÔöÇÔöÇ ┬À types(er : List),
Ôöé ┬À (er == {{ #loc, #offset }}), (#loc, l-nth(er, 0i)); (#offset, l-nth(er, 1i))
Ôöé ┬À (out == {{ #loc, (el i+ #offset) }}), (out, {{ #loc,
(el i+ #offset) }})
Ôöé ===FINISHED=== POST: None
Ôöé
ÔööÔöÇÔöÇ┬À types(er : Int),
┬À (out == (el i+ er)), (out, (el i+ er))
===FINISHED=== POST: None
Attempting to create MP of predicate i__pred_minus
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : List, er : Int) *
(el == {{ #loc, #offset }}) *
(out == {{ #loc, ((-1i i* er) i+ #offset) }})
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : List)
types(PVar er : Int)
(PVar el == {{ LVar #loc, LVar #offset }})
(PVar out ==
{{ LVar #loc, ((Lit -1i i* PVar er) i+ LVar #offset) }})
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : List), ]
TO VISIT: types(PVar er : Int)
(PVar el == {{ LVar #loc, LVar #offset }})
(PVar out ==
{{ LVar #loc, ((Lit -1i i* PVar er) i+ LVar #offset) }})
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : Int), ; types(el : List), ]
TO VISIT: (PVar el == {{ LVar #loc, LVar #offset }})
(PVar out ==
{{ LVar #loc, ((Lit -1i i* PVar er) i+ LVar #offset) }})
IO Equality: (el == {{ #loc, #offset }})
Ins: [{PVar el, LVar #loc, LVar #offset}]
KB: {PVar el, PVar er}
Known left: true Known right: false
List of expressions: [(#loc, l-nth(el, 0i)); (#offset, l-nth(el, 1i))]
Result: [({PVar el}, (#loc, l-nth(el, 0i)); (#offset, l-nth(el, 1i)))]
KNOWN: {PVar el, PVar er, LVar #loc, LVar #offset}.
CUR MP:
[(el == {{ #loc, #offset }}), (#loc, l-nth(el, 0i)); (#offset, l-nth(el, 1i));
types(er : Int), ; types(el : List), ]
TO VISIT: (PVar out ==
{{ LVar #loc, ((Lit -1i i* PVar er) i+ LVar #offset) }})
IO Equality: (out == {{ #loc, ((-1i i* er) i+ #offset) }})
Ins: [{PVar er, PVar out, LVar #loc, LVar #offset}]
KB: {PVar el, PVar er, LVar #loc, LVar #offset}
Known left: false Known right: true
Result: [({PVar er, LVar #loc, LVar #offset},
(out, {{ #loc, ((-1i i* er) i+ #offset) }}))]
KNOWN: {PVar el, PVar er, PVar out, LVar #loc, LVar #offset}.
CUR MP:
[(out == {{ #loc, ((-1i i* er) i+ #offset) }}), (out, {{ #loc,
((-1i i* er) i+ #offset) }});
(el == {{ #loc, #offset }}), (#loc, l-nth(el, 0i)); (#offset, l-nth(el, 1i));
types(er : Int), ; types(el : List), ]
TO VISIT:
Successfully created MP.
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : Int, er : Int) *
(out == (el i+ (-1i i* er)))
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : Int)
types(PVar er : Int)
(PVar out == (PVar el i+ (Lit -1i i* PVar er)))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : Int), ]
TO VISIT: types(PVar er : Int)
(PVar out == (PVar el i+ (Lit -1i i* PVar er)))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : Int), ; types(el : Int), ]
TO VISIT: (PVar out == (PVar el i+ (Lit -1i i* PVar er)))
IO Equality: (out == (el i+ (-1i i* er)))
Ins: [{PVar el, PVar er, PVar out}]
KB: {PVar el, PVar er}
Known left: false Known right: true
Result: [({PVar el, PVar er}, (out, (el i+ (-1i i* er))))]
KNOWN: {PVar el, PVar er, PVar out}.
CUR MP:
[(out == (el i+ (-1i i* er))), (out, (el i+ (-1i i* er)));
types(er : Int), ; types(el : Int), ]
TO VISIT:
Successfully created MP.
Successfully created MP of predicate i__pred_minus:
CHOICE
Ôö£ÔöÇÔöÇ ┬À types(el : List),
Ôöé ┬À types(er : Int),
Ôöé ┬À (el == {{ #loc, #offset }}), (#loc, l-nth(el, 0i)); (#offset, l-nth(el, 1i))
Ôöé ┬À (out == {{ #loc, ((-1i i* er) i+ #offset) }}), (out, {{ #loc,
((-1i i* er) i+ #offset) }})
Ôöé ===FINISHED=== POST: None
Ôöé
ÔööÔöÇÔöÇ┬À types(el : Int),
┬À types(er : Int),
┬À (out == (el i+ (-1i i* er))), (out, (el i+ (-1i i* er)))
===FINISHED=== POST: None
Attempting to create MP of predicate i__pred_geq
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : List, er : List) *
(el == {{ #locl, #offsetl }}) * (er == {{ #locr, #offsetr }}) *
(#locr == #locl) *
(out == (not (#offsetl i< #offsetr)))
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : List)
types(PVar er : List)
(PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (not (#offsetl i< #offsetr)))
(LVar #locr == LVar #locl)
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : List), ]
TO VISIT: types(PVar er : List)
(PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (not (#offsetl i< #offsetr)))
(LVar #locr == LVar #locl)
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : List), ; types(el : List), ]
TO VISIT: (PVar el == {{ LVar #locl, LVar #offsetl }})
(PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (not (#offsetl i< #offsetr)))
(LVar #locr == LVar #locl)
IO Equality: (el == {{ #locl, #offsetl }})
Ins: [{PVar el, LVar #locl, LVar #offsetl}]
KB: {PVar el, PVar er}
Known left: true Known right: false
List of expressions: [(#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i))]
Result: [({PVar el}, (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i)))]
KNOWN: {PVar el, PVar er, LVar #locl, LVar #offsetl}.
CUR MP:
[(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (PVar er == {{ LVar #locr, LVar #offsetr }})
(PVar out == (not (#offsetl i< #offsetr)))
(LVar #locr == LVar #locl)
IO Equality: (er == {{ #locr, #offsetr }})
Ins: [{PVar er, LVar #locr, LVar #offsetr}]
KB: {PVar el, PVar er, LVar #locl, LVar #offsetl}
Known left: true Known right: false
List of expressions: [(#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i))]
Result: [({PVar er}, (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i)))]
KNOWN: {PVar el, PVar er, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (PVar out == (not (#offsetl i< #offsetr)))
(LVar #locr == LVar #locl)
IO Equality: (out == (not (#offsetl i< #offsetr)))
Ins: [{PVar out, LVar #offsetl, LVar #offsetr}]
KB: {PVar el, PVar er, LVar #locl, LVar #locr, LVar #offsetl, LVar #offsetr}
Known left: false Known right: true
Result: [({LVar #offsetl, LVar #offsetr},
(out, (not (#offsetl i< #offsetr))))]
KNOWN: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(out == (not (#offsetl i< #offsetr))), (out, (not (#offsetl i< #offsetr)));
(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT: (LVar #locr == LVar #locl)
IO Equality: (#locr == #locl)
Ins: [{LVar #locl, LVar #locr}]
KB: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}
Known left: true Known right: true
KNOWN: {PVar el, PVar er, PVar out, LVar #locl, LVar #locr, LVar #offsetl,
LVar #offsetr}.
CUR MP:
[(#locr == #locl), ;
(out == (not (#offsetl i< #offsetr))), (out, (not (#offsetl i< #offsetr)));
(er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i));
(el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i));
types(er : List), ; types(el : List), ]
TO VISIT:
Successfully created MP.
Known matchables: {PVar el, PVar er}
Existentials: {}
Entering s-init on: types(el : Int, er : Int) *
(out == (not (el i< er)))
KB: {PVar el, PVar er}
KNOWN: {PVar el, PVar er}.
CUR MP:
[]
TO VISIT: types(PVar el : Int)
types(PVar er : Int)
(PVar out == (not (el i< er)))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(el : Int), ]
TO VISIT: types(PVar er : Int)
(PVar out == (not (el i< er)))
KNOWN: {PVar el, PVar er}.
CUR MP:
[types(er : Int), ; types(el : Int), ]
TO VISIT: (PVar out == (not (el i< er)))
IO Equality: (out == (not (el i< er)))
Ins: [{PVar el, PVar er, PVar out}]
KB: {PVar el, PVar er}
Known left: false Known right: true
Result: [({PVar el, PVar er}, (out, (not (el i< er))))]
KNOWN: {PVar el, PVar er, PVar out}.
CUR MP:
[(out == (not (el i< er))), (out, (not (el i< er))); types(er : Int), ;
types(el : Int), ]
TO VISIT:
Successfully created MP.
Successfully created MP of predicate i__pred_geq:
CHOICE
Ôö£ÔöÇÔöÇ ┬À types(el : List),
Ôöé ┬À types(er : List),
Ôöé ┬À (el == {{ #locl, #offsetl }}), (#locl, l-nth(el, 0i)); (#offsetl, l-nth(el, 1i))
Ôöé ┬À (er == {{ #locr, #offsetr }}), (#locr, l-nth(er, 0i)); (#offsetr, l-nth(er, 1i))
Ôöé ┬À (out == (not (#offsetl i< #offsetr))), (out, (not (#offsetl i< #offsetr)))
Ôöé ┬À (#locr == #locl),
Ôöé ===FINISHED=== POST: None
Ôöé
ÔööÔöÇÔöÇ┬À types(el : Int),
┬À types(er : Int),
┬À (out == (not (el i< er))), (out, (not (el i< er)))
===FINISHED=== POST: None
-------------------------------------------------------------------------
Creating symbolic tests for procedure llen: 1 cases
-------------------------------------------------------------------------
Normalising assertion:
types(#alpha : List) *
(x == #x) *
list(#x, #alpha)
svars: #alpha, #x
Separate assertion subst: [ ]
Here are the pfs: (x == #x)
Normalising types: 1
#alpha : List
PVars in normalise_pvar_equalities: x
Going to fill the store now.
Filled store.
About to simplify.
PFS/Gamma simplification:
With matching: Yes
PFS:
Gamma:
(#alpha: List)
PFS/Gamma simplification completed:
PFS:
Gamma:
(#alpha: List)
Done simplifying.
Finished normalising pure assertions.
Here is the store: (x: LVar #x)
pfs after overlapping constraints:
Subst:
[ ]
Subst':
[ ]
Subst before extenzion:
[ ]
PFS after extenzion:
Subst in produce asrts:
[ ]
CORE ASSERTIONS TO PRODUCE: []
Entering FOSolver.check_satisfiability
PFS/Gamma simplification:
With matching: No
PFS:
((typeOf #alpha) == List)
Gamma:
(#alpha: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len #alpha))
Gamma:
(#alpha: List)
SAT check not found in cache.
About to check SAT of:
(0i i<=# (l-len #alpha))
with gamma:
(hashtbl (#alpha, List))
Reached Z3.
The solver returned: satisfiable
Adding to cache : (0i i<=# (l-len #alpha))
-----------------------------------
STATE BEFORE SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
((typeOf #alpha) == List)
TYPING ENVIRONMENT:
(#alpha: List)
-----------------------------------
PFS/Gamma simplification:
With matching: Yes
PFS:
((typeOf #alpha) == List)
Gamma:
(#alpha: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len #alpha))
Gamma:
(#alpha: List)
Filtered and fixed subst, to be applied to memory:
[ ]
Substitution results in 1 results:
-----------------------------------
STATE AFTER SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
with substitution:
[ ]
-----------------------------------
AFTER NORMALISATION: 1 states:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
PREDICATES:
list(#x, #alpha)
WANDS:
VARIANTS:
Processing one postcondition of llen with label None and spec_vars: #alpha, #x.
Original Pre:
(x == #x) * types(#alpha : List) *
list(#x, #alpha)
Symb State Pre:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
PREDICATES:
list(#x, #alpha)
WANDS:
VARIANTS:
llen,
Subst:
[ ]
Posts (1):
types(#alpha : List) * list(#x, #alpha) *
(ret == (l-len #alpha))
Creating MPs for posts of llen
Known matchables: {PVar ret, PVar x, LVar #alpha, LVar #x}
Existentials: {}
Entering s-init on: types(#alpha : List) * list(#x, #alpha) *
(ret == (l-len #alpha))
KB: {PVar ret, PVar x, LVar #alpha, LVar #x}
KNOWN: {PVar ret, PVar x, LVar #alpha, LVar #x}.
CUR MP:
[]
TO VISIT: types(LVar #alpha : List)
(PVar ret == (l-len #alpha))
list(LVar #x, LVar #alpha)
KNOWN: {PVar ret, PVar x, LVar #alpha, LVar #x}.
CUR MP:
[types(#alpha : List), ]
TO VISIT: (PVar ret == (l-len #alpha))
list(LVar #x, LVar #alpha)
IO Equality: (ret == (l-len #alpha))
Ins: [{PVar ret, LVar #alpha}; {PVar ret, (l-len #alpha)}]
KB: {PVar ret, PVar x, LVar #alpha, LVar #x}
Known left: true Known right: true
KNOWN: {PVar ret, PVar x, LVar #alpha, LVar #x}.
CUR MP:
[(ret == (l-len #alpha)), ; types(#alpha : List), ]
TO VISIT: list(LVar #x, LVar #alpha)
Ins_and_outs_from_lists:
Ins: [#x]
Outs: [#alpha]
Calculated ins: [{LVar #x}]
KNOWN: {PVar ret, PVar x, LVar #alpha, LVar #x}.
CUR MP:
[list(#x, #alpha), ; (ret == (l-len #alpha)), ; types(#alpha : List), ]
TO VISIT:
Successfully created MP.
END of STEP 4
Simplified SPECS:
spec llen(x)
[[ (x == #x) *
(0i i<=# (l-len #alpha)) *
types(#alpha : List) *
list(#x, #alpha) ]]
[[ types(#alpha : List) * list(#x, #alpha) * (ret == (l-len #alpha)) ]]
normal
-------------------------------------------------------------------------
UNFOLDED and SIMPLIFIED SPECS and LEMMAS
spec llen(x)
[[ (x == #x) *
(0i i<=# (l-len #alpha)) *
types(#alpha : List) *
list(#x, #alpha) ]]
[[ types(#alpha : List) * list(#x, #alpha) * (ret == (l-len #alpha)) ]]
normal
-------------------------------------------------------------------------
Calculating MPs for lemmas
Attempting to create MP for a spec of llen : 1 specs
lab of sspec 0:
Known matchables: {PVar x}
Existentials: {}
Entering s-init on: (x == #x) * (0i i<=# (l-len #alpha)) *
types(#alpha : List) *
list(#x, #alpha)
KB: {PVar x}
KNOWN: {PVar x}.
CUR MP:
[]
TO VISIT: types(LVar #alpha : List)
(PVar x == LVar #x)
(Lit 0i i<=# (l-len #alpha))
list(LVar #x, LVar #alpha)
IO Equality: (x == #x)
Ins: [{PVar x, LVar #x}]
KB: {PVar x}
Known left: true Known right: false
Result: [({PVar x}, (#x, x))]
KNOWN: {PVar x, LVar #x}.
CUR MP:
[(x == #x), (#x, x)]
TO VISIT: types(LVar #alpha : List)
(Lit 0i i<=# (l-len #alpha))
list(LVar #x, LVar #alpha)
Ins_and_outs_from_lists:
Ins: [#x]
Outs: [#alpha]
Calculated ins: [{LVar #x}]
KNOWN: {PVar x, LVar #alpha, LVar #x}.
CUR MP:
[list(#x, #alpha), (#alpha, 0); (x == #x), (#x, x)]
TO VISIT: types(LVar #alpha : List)
(Lit 0i i<=# (l-len #alpha))
KNOWN: {PVar x, LVar #alpha, LVar #x}.
CUR MP:
[types(#alpha : List), ; list(#x, #alpha), (#alpha, 0); (x == #x), (#x, x)]
TO VISIT: (Lit 0i i<=# (l-len #alpha))
KNOWN: {PVar x, LVar #alpha, LVar #x}.
CUR MP:
[(0i i<=# (l-len #alpha)), ; types(#alpha : List), ;
list(#x, #alpha), (#alpha, 0); (x == #x), (#x, x)]
TO VISIT:
Successfully created MP.
Successfully created MP of specification of llen
*******************************************
*** Executing procedure: llen
*******************************************
------------------------------------------------------
--llen: 0--
TIME: 0.033274
CMD: goto [(x = null)] 1 3
LOC: llen.wisl:8:4
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 0
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
PREDICATES:
list(#x, #alpha)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Evaluated expressions: (#x = null), (not (#x = null))
SState: sat_check: (#x = null)
Entering FOSolver.check_satisfiability
PFS/Gamma simplification:
With matching: No
PFS:
(#x == null)
Gamma:
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
SState: sat_check done: true
SState: sat_check: (not (#x = null))
Entering FOSolver.check_satisfiability
PFS/Gamma simplification:
With matching: No
PFS:
(! (#x == null))
Gamma:
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(! (#x == null))
Gamma:
SAT check not found in cache.
About to check SAT of:
(! (#x == null))
with gamma:
(hashtbl )
Reached Z3.
The solver returned: satisfiable
Adding to cache : (! (#x == null))
SState: sat_check done: true
Assuming expression: (#x = null)
Starting unfold_with_vals: #x, null
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
list(#x, #alpha)
WANDS:
VARIANTS:
llen,
.
Strategy 1: Examining list(#x, #alpha)
Original values: [#x, null]
Extended values: [null, #x]
get_pred_with_vs. Strategy 1. Intersection of cardinal 1: [#x]
FOUND STH TO UNFOLD: list!!!!
Combine going to explode. PredName: list. Params: x, alpha]. Args: #x, #alpha
unfold with unfold_info with additional bindings
[]
Using unfold info, obtained subst:
[ (alpha: #alpha), (x: #x) ]
Going to produce 2 definitions with subst
[ (alpha: #alpha), (x: #x) ]
-----------------
-----------------
Produce assertion: types(alpha : List, #beta : List, #wisl__0 : Obj,
#wisl__1 : Int) *
<cell>(#wisl__0, #wisl__1; #v) *
<cell>(#wisl__0, (1i i+ #wisl__1); #z) *
(x == {{ #wisl__0, #wisl__1 }}) * list(#z, #beta) *
(alpha == l+ ({{ #v }}, #beta))
-------------------------
Produce simple assertion: types(alpha : List)
With subst: [ (alpha: #alpha), (x: #x) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: types(#beta : List)
With subst: [ (alpha: #alpha), (x: #x) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: types(#wisl__0 : Obj)
With subst: [ (alpha: #alpha), (x: #x), (#beta: _lvar_0) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_0: List)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: types(#wisl__1 : Int)
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_0),
(#wisl__0: _lvar_1) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_0: List)
(_lvar_1: Obj)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: <cell>(#wisl__0, #wisl__1; #v)
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_0),
(#wisl__0: _lvar_1),
(#wisl__1: _lvar_2) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_0: List)
(_lvar_1: Obj)
(_lvar_2: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Memory producer.
-------------------------
Produce simple assertion: <cell>(#wisl__0, (1i i+ #wisl__1); #z)
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_0),
(#v: _lvar_3),
(#wisl__0: _lvar_1),
(#wisl__1: _lvar_2) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_0 -> BOUND: NONE
{_lvar_2: _lvar_3}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
(_$l_0 == _lvar_1)
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_0: List)
(_lvar_1: Obj)
(_lvar_2: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Memory producer.
-------------------------
Produce simple assertion: (x == {{ #wisl__0, #wisl__1 }})
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_0),
(#v: _lvar_3),
(#wisl__0: _lvar_1),
(#wisl__1: _lvar_2),
(#z: _lvar_4) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_0 -> BOUND: NONE
{_lvar_2: _lvar_3
(1i i+ _lvar_2): _lvar_4}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
(_$l_0 == _lvar_1)
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_0: List)
(_lvar_1: Obj)
(_lvar_2: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Pure assertion.
-------------------------
Produce simple assertion: list(#z, #beta)
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_0),
(#v: _lvar_3),
(#wisl__0: _lvar_1),
(#wisl__1: _lvar_2),
(#z: _lvar_4) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_0 -> BOUND: NONE
{_lvar_2: _lvar_3
(1i i+ _lvar_2): _lvar_4}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
(_$l_0 == _lvar_1)
(#x == {{ _lvar_1, _lvar_2 }})
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_0: List)
(_lvar_1: Obj)
(_lvar_2: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Predicate assertion.
-------------------------
Produce simple assertion: ((typeOf #beta) == List)
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_0),
(#v: _lvar_3),
(#wisl__0: _lvar_1),
(#wisl__1: _lvar_2),
(#z: _lvar_4) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_0 -> BOUND: NONE
{_lvar_2: _lvar_3
(1i i+ _lvar_2): _lvar_4}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
(_$l_0 == _lvar_1)
(#x == {{ _lvar_1, _lvar_2 }})
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_0: List)
(_lvar_1: Obj)
(_lvar_2: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Pure assertion.
-------------------------
Produce simple assertion: (alpha == l+ ({{ #v }}, #beta))
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_0),
(#v: _lvar_3),
(#wisl__0: _lvar_1),
(#wisl__1: _lvar_2),
(#z: _lvar_4) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_0 -> BOUND: NONE
{_lvar_2: _lvar_3
(1i i+ _lvar_2): _lvar_4}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
(_$l_0 == _lvar_1)
(#x == {{ _lvar_1, _lvar_2 }})
True
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_0: List)
(_lvar_1: Obj)
(_lvar_2: Int)
PREDS:
list(_lvar_4, _lvar_0)
WANDS:
VARIANTS:
llen,
Pure assertion.
Produce: final check
Entering FOSolver.check_satisfiability
PFS/Gamma simplification:
With matching: Yes
PFS:
True
(0i i<=# (l-len #alpha))
(#x == null)
(_$l_0 == _lvar_1)
(#x == {{ _lvar_1, _lvar_2 }})
True
(#alpha == l+ ({{ _lvar_3 }}, _lvar_0))
Gamma:
(#alpha: List)
(_lvar_0: List)
(_lvar_1: Obj)
(_lvar_2: Int)
Pure formulae false: False in pure formulae
Pure formulae false: False in pure formulae
PFS/Gamma simplification completed:
PFS:
False
Gamma:
(#alpha: List)
(_lvar_0: List)
(_lvar_2: Int)
assume_a: Couldn't assume [True]
Concluded final check
-----------------
-----------------
Produce assertion: types(alpha : List) * (x == null) * (alpha == {{ }})
-------------------------
Produce simple assertion: types(alpha : List)
With subst: [ (alpha: #alpha), (x: #x) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: (x == null)
With subst: [ (alpha: #alpha), (x: #x) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
WANDS:
VARIANTS:
llen,
Pure assertion.
-------------------------
Produce simple assertion: (alpha == {{ }})
With subst: [ (alpha: #alpha), (x: #x) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
WANDS:
VARIANTS:
llen,
Pure assertion.
Produce: final check
Entering FOSolver.check_satisfiability
PFS/Gamma simplification:
With matching: Yes
PFS:
True
(0i i<=# (l-len #alpha))
(#x == null)
(#alpha == {{ }})
Gamma:
(#alpha: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
Concluded final check
-----------------------------------
STATE BEFORE SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(#x == null)
(#alpha == {{ }})
True
TYPING ENVIRONMENT:
(#alpha: List)
-----------------------------------
PFS/Gamma simplification:
With matching: Yes
PFS:
(0i i<=# (l-len #alpha))
(#x == null)
(#alpha == {{ }})
True
Gamma:
(#alpha: List)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
Gamma:
(#alpha: List)
(#x: Null)
Filtered and fixed subst, to be applied to memory:
[ ]
Substitution results in 1 results:
-----------------------------------
STATE AFTER SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
with substitution:
[ ]
-----------------------------------
Warning: (StateErr.EOther "final state non admissible")
Results of unfolding list(x, alpha):
Result 0
STATE:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDS:
WANDS:
VARIANTS:
llen,
SUBST:[ ]
Unfold complete: list(#x, #alpha): 1
-----------------------------------
STATE BEFORE SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
-----------------------------------
PFS/Gamma simplification:
With matching: No
PFS:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
Gamma:
(#alpha: List)
(#x: Null)
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
Gamma:
(#alpha: List)
(#x: Null)
Filtered and fixed subst, to be applied to memory:
[ ]
Substitution results in 1 results:
-----------------------------------
STATE AFTER SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
with substitution:
[ ]
-----------------------------------
Assuming expression: (not (#x = null))
Starting unfold_with_vals: #x, null
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
list(#x, #alpha)
WANDS:
VARIANTS:
llen,
.
Strategy 1: Examining list(#x, #alpha)
Original values: [#x, null]
Extended values: [null, #x]
get_pred_with_vs. Strategy 1. Intersection of cardinal 1: [#x]
FOUND STH TO UNFOLD: list!!!!
Combine going to explode. PredName: list. Params: x, alpha]. Args: #x, #alpha
unfold with unfold_info with additional bindings
[]
Using unfold info, obtained subst:
[ (alpha: #alpha), (x: #x) ]
Going to produce 2 definitions with subst
[ (alpha: #alpha), (x: #x) ]
-----------------
-----------------
Produce assertion: types(alpha : List, #beta : List, #wisl__0 : Obj,
#wisl__1 : Int) *
<cell>(#wisl__0, #wisl__1; #v) *
<cell>(#wisl__0, (1i i+ #wisl__1); #z) *
(x == {{ #wisl__0, #wisl__1 }}) * list(#z, #beta) *
(alpha == l+ ({{ #v }}, #beta))
-------------------------
Produce simple assertion: types(alpha : List)
With subst: [ (alpha: #alpha), (x: #x) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: types(#beta : List)
With subst: [ (alpha: #alpha), (x: #x) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: types(#wisl__0 : Obj)
With subst: [ (alpha: #alpha), (x: #x), (#beta: _lvar_5) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_5: List)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: types(#wisl__1 : Int)
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_5),
(#wisl__0: _lvar_6) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_5: List)
(_lvar_6: Obj)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: <cell>(#wisl__0, #wisl__1; #v)
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_5),
(#wisl__0: _lvar_6),
(#wisl__1: _lvar_7) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Memory producer.
-------------------------
Produce simple assertion: <cell>(#wisl__0, (1i i+ #wisl__1); #z)
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_5),
(#v: _lvar_8),
(#wisl__0: _lvar_6),
(#wisl__1: _lvar_7) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
(_$l_1 == _lvar_6)
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Memory producer.
-------------------------
Produce simple assertion: (x == {{ #wisl__0, #wisl__1 }})
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_5),
(#v: _lvar_8),
(#wisl__0: _lvar_6),
(#wisl__1: _lvar_7),
(#z: _lvar_9) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
(_$l_1 == _lvar_6)
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Pure assertion.
-------------------------
Produce simple assertion: list(#z, #beta)
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_5),
(#v: _lvar_8),
(#wisl__0: _lvar_6),
(#wisl__1: _lvar_7),
(#z: _lvar_9) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
(_$l_1 == _lvar_6)
(#x == {{ _lvar_6, _lvar_7 }})
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Predicate assertion.
-------------------------
Produce simple assertion: ((typeOf #beta) == List)
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_5),
(#v: _lvar_8),
(#wisl__0: _lvar_6),
(#wisl__1: _lvar_7),
(#z: _lvar_9) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
(_$l_1 == _lvar_6)
(#x == {{ _lvar_6, _lvar_7 }})
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Pure assertion.
-------------------------
Produce simple assertion: (alpha == l+ ({{ #v }}, #beta))
With subst: [ (alpha: #alpha),
(x: #x),
(#beta: _lvar_5),
(#v: _lvar_8),
(#wisl__0: _lvar_6),
(#wisl__1: _lvar_7),
(#z: _lvar_9) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
(_$l_1 == _lvar_6)
(#x == {{ _lvar_6, _lvar_7 }})
True
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Pure assertion.
Produce: final check
Entering FOSolver.check_satisfiability
PFS/Gamma simplification:
With matching: Yes
PFS:
True
(0i i<=# (l-len #alpha))
(! (#x == null))
(_$l_1 == _lvar_6)
(#x == {{ _lvar_6, _lvar_7 }})
True
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
Gamma:
(#alpha: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len _lvar_5))
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check not found in cache.
About to check SAT of:
(0i i<=# (l-len _lvar_5))
with gamma:
(hashtbl (_lvar_7, Int) (_lvar_5, List))
Reached Z3.
The solver returned: satisfiable
Adding to cache : (0i i<=# (l-len _lvar_5))
Concluded final check
-----------------
-----------------
Produce assertion: types(alpha : List) * (x == null) * (alpha == {{ }})
-------------------------
Produce simple assertion: types(alpha : List)
With subst: [ (alpha: #alpha), (x: #x) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: (x == null)
With subst: [ (alpha: #alpha), (x: #x) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
WANDS:
VARIANTS:
llen,
Pure assertion.
-------------------------
Produce simple assertion: (alpha == {{ }})
With subst: [ (alpha: #alpha), (x: #x) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
(#x == null)
TYPING ENVIRONMENT:
(#alpha: List)
PREDS:
WANDS:
VARIANTS:
llen,
Pure assertion.
Produce: final check
Entering FOSolver.check_satisfiability
PFS/Gamma simplification:
With matching: Yes
PFS:
True
(0i i<=# (l-len #alpha))
(! (#x == null))
(#x == null)
(#alpha == {{ }})
Gamma:
(#alpha: List)
Pure formulae false: False in pure formulae
Pure formulae false: False in pure formulae
PFS/Gamma simplification completed:
PFS:
False
Gamma:
assume_a: Couldn't assume [True]
Concluded final check
Warning: (StateErr.EOther "final state non admissible")
-----------------------------------
STATE BEFORE SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(0i i<=# (l-len #alpha))
(! (#x == null))
(_$l_1 == _lvar_6)
(#x == {{ _lvar_6, _lvar_7 }})
True
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
-----------------------------------
PFS/Gamma simplification:
With matching: Yes
PFS:
(0i i<=# (l-len #alpha))
(! (#x == null))
(_$l_1 == _lvar_6)
(#x == {{ _lvar_6, _lvar_7 }})
True
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
Gamma:
(#alpha: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
Filtered and fixed subst, to be applied to memory:
[ (_lvar_6: _$l_1) ]
Substitution results in 1 results:
-----------------------------------
STATE AFTER SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
with substitution:
[ (_lvar_6: _$l_1) ]
-----------------------------------
Results of unfolding list(x, alpha):
Result 0
STATE:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
SUBST:[ (_lvar_6: _$l_1) ]
Unfold complete: list(#x, #alpha): 1
-----------------------------------
STATE BEFORE SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
-----------------------------------
PFS/Gamma simplification:
With matching: No
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
Filtered and fixed subst, to be applied to memory:
[ (_lvar_6: _$l_1) ]
Substitution results in 1 results:
-----------------------------------
STATE AFTER SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
with substitution:
[ (_lvar_6: _$l_1) ]
-----------------------------------
------------------------------------------------------
--llen: 1--
TIME: 0.036179
CMD: n := 1i
LOC: llen.wisl:9:8
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDICATES:
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--llen: 2--
TIME: 0.036216
CMD: goto 11
LOC: llen.wisl:8:4
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(n: Lit 1i)
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDICATES:
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--llen: 11--
TIME: 0.036248
CMD: skip
LOC: llen.wisl:8:4
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(n: Lit 1i)
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDICATES:
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--llen: 12--
TIME: 0.036270
CMD: ret := n
LOC: llen.wisl:15:11
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(n: Lit 1i)
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDICATES:
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--llen: 13--
TIME: 0.036521
CMD: return
LOC: llen.wisl:15:11
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(n: Lit 1i)
(ret: Lit 1i)
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDICATES:
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Returning.
------------------------------------------------------
--llen: 3--
TIME: 0.036561
CMD: gvar0 := "i__add"(x, 1i)
LOC: llen.wisl:11:14
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--i__add: 0--
TIME: 0.036605
CMD: goto [(((typeOf el) = List) and ((typeOf er) = Int))] 1 3
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:15:8
PROCS: [i__add, llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(el: LVar #x)
(er: Lit 1i)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Evaluated expressions: true, false
Assuming expression: true
------------------------------------------------------
--i__add: 1--
TIME: 0.036666
CMD: ret := "i__ptr_add"(el, er)
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:17:8
PROCS: [i__add, llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(el: LVar #x)
(er: Lit 1i)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--i__ptr_add: 0--
TIME: 0.036709
CMD: loc := l-nth(ptr, 0i)
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:8:2
PROCS: [i__ptr_add, i__add, llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(add_offset: Lit 1i)
(ptr: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--i__ptr_add: 1--
TIME: 0.036753
CMD: offset := l-nth(ptr, 1i)
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:9:2
PROCS: [i__ptr_add, i__add, llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(add_offset: Lit 1i)
(loc: ALoc _$l_1)
(ptr: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--i__ptr_add: 2--
TIME: 0.036801
CMD: ret := {{ loc, (offset i+ add_offset) }}
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:10:2
PROCS: [i__ptr_add, i__add, llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(add_offset: Lit 1i)
(loc: ALoc _$l_1)
(offset: LVar _lvar_7)
(ptr: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--i__ptr_add: 3--
TIME: 0.036851
CMD: return
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:11:2
PROCS: [i__ptr_add, i__add, llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(add_offset: Lit 1i)
(loc: ALoc _$l_1)
(offset: LVar _lvar_7)
(ptr: LVar #x)
(ret: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Returning.
------------------------------------------------------
--i__add: 2--
TIME: 0.036901
CMD: return
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:18:8
PROCS: [i__add, llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(el: LVar #x)
(er: Lit 1i)
(ret: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Returning.
------------------------------------------------------
--llen: 4--
TIME: 0.036945
CMD: goto [((typeOf gvar0) = List)] 6 5
LOC: llen.wisl:11:8
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Evaluated expressions: true, false
Assuming expression: true
-----------------------------------
STATE BEFORE SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
-----------------------------------
PFS/Gamma simplification:
With matching: No
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
Filtered and fixed subst, to be applied to memory:
[ (_lvar_6: _$l_1) ]
Substitution results in 1 results:
-----------------------------------
STATE AFTER SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
with substitution:
[ (_lvar_6: _$l_1) ]
-----------------------------------
------------------------------------------------------
--llen: 6--
TIME: 0.037172
CMD: gvar1 := [getcell](l-nth(gvar0, 0i), l-nth(gvar0, 1i))
LOC: llen.wisl:11:8
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--llen: 7--
TIME: 0.037228
CMD: t := l-nth(gvar1, 2i)
LOC: llen.wisl:11:8
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(gvar1: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7), LVar _lvar_9 }})
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--llen: 8--
TIME: 0.037278
CMD: n := "llen"(t)
LOC: llen.wisl:12:8
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 1
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(gvar1: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7), LVar _lvar_9 }})
(t: LVar _lvar_9)
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
ABOUT TO USE THE SPEC OF llen
INSIDE RUN spec of llen with the following MP:
┬À (x == #x), (#x, x)
┬À list(#x, #alpha), (#alpha, 0)
┬À types(#alpha : List),
┬À (0i i<=# (l-len #alpha)),
===FINISHED=== POST: Some
normal: types(#alpha : List) * list(#x, #alpha) *
(ret == (l-len #alpha))
About to use the spec of llen with the following MP:
┬À (x == #x), (#x, x)
┬À list(#x, #alpha), (#alpha, 0)
┬À types(#alpha : List),
┬À (0i i<=# (l-len #alpha)),
===FINISHED=== POST: Some
normal: types(#alpha : List) * list(#x, #alpha) *
(ret == (l-len #alpha))
Matcher.match_: about to match MP.
Match MP: There are 1 states left to consider.
Substs:
[]
[_lvar_9]
[]
Match assertion: (x == #x), (#x, x)
Subst:
[ (x: _lvar_9) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(x: LVar _lvar_9)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(_lvar_9 == _lvar_9)
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len _lvar_5))
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
PFS/Gamma simplification:
With matching: No
PFS:
False
(0i i<=# (l-len _lvar_5))
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
Pure formulae false: False in pure formulae
Pure formulae false: False in pure formulae
PFS/Gamma simplification completed:
PFS:
False
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check not found in cache.
About to check SAT of:
False
with gamma:
(hashtbl (_lvar_7, Int) (_lvar_5, List))
Reached Z3.
The solver returned: unsatisfiable
Adding to cache : False
Entailment returned true
Match MP: There are 1 states left to consider.
Substs:
[]
[_lvar_9]
[]
Match assertion: list(#x, #alpha), (#alpha, 0)
Subst:
[ (x: _lvar_9), (#x: _lvar_9) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(x: LVar _lvar_9)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Matching predicate assertion
ARGS: #x,
#alpha
SUBST:
[ (x: _lvar_9), (#x: _lvar_9) ]
Looking for ins: [_lvar_9]
Preds.consume_pred: Looking for: list[Some _lvar_9; None]
Found 1 candidates:
[_lvar_9; _lvar_5]
Returning the following vs: _lvar_9, _lvar_5
learned the outs of a predicate. going to match (_lvar_5) against (#alpha)!!!
Outs: [(#alpha, PVar 0)]
Obtained values: [_lvar_5]
Obtained exprs: [#alpha]
Parameter subst
[ (0: _lvar_5) ]
Substed outs: [(#alpha, LVar _lvar_5)]
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(_lvar_5 == _lvar_5)
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Match MP: There are 1 states left to consider.
Substs:
[]
[_lvar_5]
[]
Match assertion: types(#alpha : List),
Subst:
[ (x: _lvar_9), (#alpha: _lvar_5), (#x: _lvar_9) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(x: LVar _lvar_9)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Match MP: There are 1 states left to consider.
Substs:
[]
[_lvar_5]
[]
Match assertion: (0i i<=# (l-len #alpha)),
Subst:
[ (x: _lvar_9), (#alpha: _lvar_5), (#x: _lvar_9) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(x: LVar _lvar_9)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Match MP: There are 1 states left to consider.
Matcher.match_mp: Matching successful: 1 states left
Matcher.match_: Success (possibly empty)
Produce posts: There are 1 postconditions to produce. And here they are:
types(#alpha : List) *
list(#x, #alpha) *
(ret == (l-len #alpha))
-----------------
-----------------
Produce assertion: types(#alpha : List) * list(#x, #alpha) *
(ret == (l-len #alpha))
-------------------------
Produce simple assertion: types(#alpha : List)
With subst: [ (x: _lvar_9), (#alpha: _lvar_5), (#x: _lvar_9) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar _lvar_9)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Types assertion.
-------------------------
Produce simple assertion: list(#x, #alpha)
With subst: [ (x: _lvar_9), (#alpha: _lvar_5), (#x: _lvar_9) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar _lvar_9)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Predicate assertion.
-------------------------
Produce simple assertion: ((typeOf #alpha) == List)
With subst: [ (x: _lvar_9), (#alpha: _lvar_5), (#x: _lvar_9) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar _lvar_9)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Pure assertion.
-------------------------
Produce simple assertion: (ret == (l-len #alpha))
With subst: [ (x: _lvar_9), (#alpha: _lvar_5), (#x: _lvar_9) ]
-------------------------
STATE: SPEC VARS: #alpha, #x
STORE:
(x: LVar _lvar_9)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
True
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Pure assertion.
UNHAPPY. update_store inside produce assertions with prog variable: ret!!!
Produce: final check
Entering FOSolver.check_satisfiability
PFS/Gamma simplification:
With matching: Yes
PFS:
True
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
True
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len _lvar_5))
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: true
Concluded final check
-----------------------------------
STATE BEFORE SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(gvar1: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7), LVar _lvar_9 }})
(n: (l-len _lvar_5))
(t: LVar _lvar_9)
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
True
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
-----------------------------------
PFS/Gamma simplification:
With matching: Yes
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(_lvar_6 == _$l_1)
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
True
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_6: Obj)
(_lvar_7: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
Filtered and fixed subst, to be applied to memory:
[ (_lvar_6: _$l_1) ]
Substitution results in 1 results:
-----------------------------------
STATE AFTER SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(gvar1: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7), LVar _lvar_9 }})
(n: (l-len _lvar_5))
(t: LVar _lvar_9)
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
with substitution:
[ (_lvar_6: _$l_1) ]
-----------------------------------
Run_spec returned 1 Results
------------------------------------------------------
--llen: 9--
TIME: 0.038526
CMD: gvar2 := "i__add"(n, 1i)
LOC: llen.wisl:13:13
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 2
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(gvar1: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7), LVar _lvar_9 }})
(n: (l-len _lvar_5))
(t: LVar _lvar_9)
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--i__add: 0--
TIME: 0.038575
CMD: goto [(((typeOf el) = List) and ((typeOf er) = Int))] 1 3
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:15:8
PROCS: [i__add, llen]
LOOPS: [] ++ []
BRANCHING: 2
SPEC VARS: #alpha, #x
STORE:
(el: (l-len _lvar_5))
(er: Lit 1i)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Evaluated expressions: false, true
Assuming expression: true
------------------------------------------------------
--i__add: 3--
TIME: 0.038635
CMD: goto [(((typeOf er) = List) and ((typeOf el) = Int))] 4 6
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:20:8
PROCS: [i__add, llen]
LOOPS: [] ++ []
BRANCHING: 2
SPEC VARS: #alpha, #x
STORE:
(el: (l-len _lvar_5))
(er: Lit 1i)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Evaluated expressions: false, true
Assuming expression: true
------------------------------------------------------
--i__add: 6--
TIME: 0.038686
CMD: goto [(((typeOf el) = Int) and ((typeOf el) = Int))] 7 9
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:25:8
PROCS: [i__add, llen]
LOOPS: [] ++ []
BRANCHING: 2
SPEC VARS: #alpha, #x
STORE:
(el: (l-len _lvar_5))
(er: Lit 1i)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Evaluated expressions: true, false
Assuming expression: true
------------------------------------------------------
--i__add: 7--
TIME: 0.038740
CMD: ret := (el i+ er)
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:26:8
PROCS: [i__add, llen]
LOOPS: [] ++ []
BRANCHING: 2
SPEC VARS: #alpha, #x
STORE:
(el: (l-len _lvar_5))
(er: Lit 1i)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--i__add: 8--
TIME: 0.038785
CMD: return
LOC: /home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/wisl/wisl_pointer_arith.gil:27:8
PROCS: [i__add, llen]
LOOPS: [] ++ []
BRANCHING: 2
SPEC VARS: #alpha, #x
STORE:
(el: (l-len _lvar_5))
(er: Lit 1i)
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Returning.
------------------------------------------------------
--llen: 10--
TIME: 0.038830
CMD: n := gvar2
LOC: llen.wisl:13:8
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 2
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(gvar1: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7), LVar _lvar_9 }})
(gvar2: (Lit 1i i+ (l-len _lvar_5)))
(n: (l-len _lvar_5))
(t: LVar _lvar_9)
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--llen: 11--
TIME: 0.038878
CMD: skip
LOC: llen.wisl:8:4
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 2
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(gvar1: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7), LVar _lvar_9 }})
(gvar2: (Lit 1i i+ (l-len _lvar_5)))
(n: (Lit 1i i+ (l-len _lvar_5)))
(t: LVar _lvar_9)
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--llen: 12--
TIME: 0.038928
CMD: ret := n
LOC: llen.wisl:15:11
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 2
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(gvar1: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7), LVar _lvar_9 }})
(gvar2: (Lit 1i i+ (l-len _lvar_5)))
(n: (Lit 1i i+ (l-len _lvar_5)))
(t: LVar _lvar_9)
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
------------------------------------------------------
--llen: 13--
TIME: 0.038976
CMD: return
LOC: llen.wisl:15:11
PROCS: [llen]
LOOPS: [] ++ []
BRANCHING: 2
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(gvar1: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7), LVar _lvar_9 }})
(gvar2: (Lit 1i i+ (l-len _lvar_5)))
(n: (Lit 1i i+ (l-len _lvar_5)))
(ret: (Lit 1i i+ (l-len _lvar_5)))
(t: LVar _lvar_9)
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
------------------------------------------------------
Returning.
Relaunching suspended confs
Verification: Concluded evaluation: 2 obtained results.RESULT: 0.
SUCCESSFUL TERMINATION: (normal, (1i i+ (l-len _lvar_5)))
FINAL STATE:
SPEC VARS: #alpha, #x
STORE:
(gvar0: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7) }})
(gvar1: {{ ALoc _$l_1, (Lit 1i i+ LVar _lvar_7), LVar _lvar_9 }})
(gvar2: (Lit 1i i+ (l-len _lvar_5)))
(n: (Lit 1i i+ (l-len _lvar_5)))
(ret: (Lit 1i i+ (l-len _lvar_5)))
(t: LVar _lvar_9)
(x: LVar #x)
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDICATES:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
RESULT: 1.
SUCCESSFUL TERMINATION: (normal, 1i)
FINAL STATE:
SPEC VARS: #alpha, #x
STORE:
(n: Lit 1i)
(ret: Lit 1i)
(x: LVar #x)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDICATES:
WANDS:
VARIANTS:
llen,
-----------------------------------
STATE BEFORE SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
-----------------------------------
PFS/Gamma simplification:
With matching: No
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
Filtered and fixed subst, to be applied to memory:
[ ]
Substitution results in 1 results:
-----------------------------------
STATE AFTER SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
with substitution:
[ ]
-----------------------------------
Analyse result: About to match one postcondition of llen. post: ┬À types(#alpha : List),
┬À (ret == (l-len #alpha)),
┬À list(#x, #alpha),
===FINISHED=== POST: None
Matcher.match_: about to match MP.
Match MP: There are 1 states left to consider.
Substs:
[]
[#alpha]
[]
Match assertion: types(#alpha : List),
Subst:
[ (ret: (1i i+ (l-len _lvar_5))), (#alpha: #alpha), (#x: #x) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Match MP: There are 1 states left to consider.
Substs:
[]
[#alpha, _lvar_5]
[]
Match assertion: (ret == (l-len #alpha)),
Subst:
[ (ret: (1i i+ (l-len _lvar_5))), (#alpha: #alpha), (#x: #x) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:((1i i+ (l-len _lvar_5)) == (l-len #alpha))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(0i i<=# (l-len _lvar_5))
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Match MP: There are 1 states left to consider.
Substs:
[]
[#alpha, #x]
[]
Match assertion: list(#x, #alpha),
Subst:
[ (ret: (1i i+ (l-len _lvar_5))), (#alpha: #alpha), (#x: #x) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Matching predicate assertion
ARGS: #x,
#alpha
SUBST:
[ (ret: (1i i+ (l-len _lvar_5))), (#alpha: #alpha), (#x: #x) ]
Looking for ins: [#x]
Preds.consume_pred: Looking for: list[Some #x; Some #alpha]
Found 1 candidates:
[_lvar_9; _lvar_5]
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(_lvar_9 == #x)
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
(_lvar_9 == {{ _$l_1, _lvar_7 }})
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: (_lvar_9 == {{ _$l_1, _lvar_7 }})
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(! (_lvar_9 == {{ _$l_1, _lvar_7 }}))
(0i i<=# (l-len _lvar_5))
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(! (_lvar_9 == {{ _$l_1, _lvar_7 }}))
(0i i<=# (l-len _lvar_5))
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check not found in cache.
About to check SAT of:
(! (_lvar_9 == {{ _$l_1, _lvar_7 }}))
(0i i<=# (l-len _lvar_5))
with gamma:
(hashtbl (_lvar_7, Int) (_lvar_5, List))
Reached Z3.
The solver returned: satisfiable
Adding to cache : ((! (_lvar_9 == {{ _$l_1, _lvar_7 }})) /\
(0i i<=# (l-len _lvar_5)))
Entailment returned false
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(_lvar_5 == #alpha)
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
(_lvar_5 == l+ ({{ _lvar_8 }}, _lvar_5))
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: (_lvar_5 == l+ ({{ _lvar_8 }}, _lvar_5))
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
PFS/Gamma simplification:
With matching: No
PFS:
(! (_lvar_5 == l+ ({{ _lvar_8 }}, _lvar_5)))
(0i i<=# (l-len _lvar_5))
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(! (_lvar_5 == l+ ({{ _lvar_8 }}, _lvar_5)))
(0i i<=# (l-len _lvar_5))
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check not found in cache.
About to check SAT of:
(! (_lvar_5 == l+ ({{ _lvar_8 }}, _lvar_5)))
(0i i<=# (l-len _lvar_5))
with gamma:
(hashtbl (_lvar_7, Int) (_lvar_5, List))
Reached Z3.
The solver returned: satisfiable
Adding to cache : ((! (_lvar_5 == l+ ({{ _lvar_8 }}, _lvar_5))) /\
(0i i<=# (l-len _lvar_5)))
Entailment returned false
Auto-folding predicate: list
Recursive case - attempting to fold.
Folding predicate: list
Predicate matching plan: CHOICE
Ôö£ÔöÇÔöÇ ┬À (alpha == {{ }}), (alpha, {{ }})
Ôöé ┬À types(alpha : List),
Ôöé ┬À (x == null),
Ôöé ===FINISHED=== POST: None
Ôöé
ÔööÔöÇÔöÇ┬À (x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))
┬À types(#wisl__0 : Obj),
┬À types(#wisl__1 : Int),
┬À <cell>(#wisl__0, #wisl__1; #v), (#v, 0)
┬À <cell>(#wisl__0, (1i i+ #wisl__1); #z), (#z, 0)
┬À list(#z, #beta), (#beta, 0)
┬À types(#beta : List),
┬À (alpha == l+ ({{ #v }}, #beta)), (alpha, l+ ({{ #v }}, #beta))
┬À types(alpha : List),
===FINISHED=== POST: None
Matcher.match_: about to match MP.
Match MP: There are 1 states left to consider.
Reached a choice with 2 MPs: about to branch
Match MP: There are 2 states left to consider.
Substs:
[]
[]
[]
Match assertion: (alpha == {{ }}), (alpha, {{ }})
Subst:
[ (x: #x) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:({{ }} == {{ }})
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Match MP: There are 2 states left to consider.
Substs:
[]
[]
[]
Match assertion: types(alpha : List),
Subst:
[ (alpha: {{ }}), (x: #x) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Match MP: There are 2 states left to consider.
Substs:
[]
[#x]
[]
Match assertion: (x == null),
Subst:
[ (alpha: {{ }}), (x: #x) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(#x == null)
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
False
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: False
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
WARNING: Match Assertion Failed: (x == null), with subst
[ (alpha: {{ }}), (x: #x) ] in state
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
with errors:
EAsrt(#x; (! (#x == null)); [(#x == null)])
Match MP: There are 1 states left to consider.
Substs:
[]
[#x]
[]
Match assertion: (x == {{ #wisl__0, #wisl__1 }}), (#wisl__0, l-nth(x, 0i)); (#wisl__1, l-nth(x, 1i))
Subst:
[ (x: #x) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(#x == {{ l-nth(#x, 0i), l-nth(#x, 1i) }})
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Match MP: There are 1 states left to consider.
Substs:
[]
[#x]
[]
Match assertion: types(#wisl__0 : Obj),
Subst:
[ (x: #x), (#wisl__0: l-nth(#x, 0i)), (#wisl__1: l-nth(#x, 1i)) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Match MP: There are 1 states left to consider.
Substs:
[]
[#x]
[]
Match assertion: types(#wisl__1 : Int),
Subst:
[ (x: #x), (#wisl__0: l-nth(#x, 0i)), (#wisl__1: l-nth(#x, 1i)) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Match MP: There are 1 states left to consider.
Substs:
[]
[#x]
[]
Match assertion: <cell>(#wisl__0, #wisl__1; #v), (#v, 0)
Subst:
[ (x: #x), (#wisl__0: l-nth(#x, 0i)), (#wisl__1: l-nth(#x, 1i)) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{_lvar_7: _lvar_8
(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Executing consume: cell with ins: _$l_1, _lvar_7
Outs: [(#v, PVar 0)]
Obtained values: [_lvar_8]
Obtained exprs: [#v]
Parameter subst
[ (0: _lvar_8) ]
Substed outs: [(#v, LVar _lvar_8)]
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(_lvar_8 == _lvar_8)
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Match MP: There are 1 states left to consider.
Substs:
[]
[#x]
[]
Match assertion: <cell>(#wisl__0, (1i i+ #wisl__1); #z), (#z, 0)
Subst:
[ (x: #x),
(#v: _lvar_8),
(#wisl__0: l-nth(#x, 0i)),
(#wisl__1: l-nth(#x, 1i)) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{(1i i+ _lvar_7): _lvar_9}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Executing consume: cell with ins: _$l_1, (1i i+ _lvar_7)
Outs: [(#z, PVar 0)]
Obtained values: [_lvar_9]
Obtained exprs: [#z]
Parameter subst
[ (0: _lvar_9) ]
Substed outs: [(#z, LVar _lvar_9)]
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(_lvar_9 == _lvar_9)
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Match MP: There are 1 states left to consider.
Substs:
[]
[_lvar_9]
[]
Match assertion: list(#z, #beta), (#beta, 0)
Subst:
[ (x: #x),
(#v: _lvar_8),
(#wisl__0: l-nth(#x, 0i)),
(#wisl__1: l-nth(#x, 1i)),
(#z: _lvar_9) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
list(_lvar_9, _lvar_5)
WANDS:
VARIANTS:
llen,
Matching predicate assertion
ARGS: #z,
#beta
SUBST:
[ (x: #x),
(#v: _lvar_8),
(#wisl__0: l-nth(#x, 0i)),
(#wisl__1: l-nth(#x, 1i)),
(#z: _lvar_9) ]
Looking for ins: [_lvar_9]
Preds.consume_pred: Looking for: list[Some _lvar_9; None]
Found 1 candidates:
[_lvar_9; _lvar_5]
Returning the following vs: _lvar_9, _lvar_5
learned the outs of a predicate. going to match (_lvar_5) against (#beta)!!!
Outs: [(#beta, PVar 0)]
Obtained values: [_lvar_5]
Obtained exprs: [#beta]
Parameter subst
[ (0: _lvar_5) ]
Substed outs: [(#beta, LVar _lvar_5)]
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(_lvar_5 == _lvar_5)
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Match MP: There are 1 states left to consider.
Substs:
[]
[_lvar_5]
[]
Match assertion: types(#beta : List),
Subst:
[ (x: #x),
(#beta: _lvar_5),
(#v: _lvar_8),
(#wisl__0: l-nth(#x, 0i)),
(#wisl__1: l-nth(#x, 1i)),
(#z: _lvar_9) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Match MP: There are 1 states left to consider.
Substs:
[]
[_lvar_5, _lvar_8]
[]
Match assertion: (alpha == l+ ({{ #v }}, #beta)), (alpha, l+ ({{ #v }},
#beta))
Subst:
[ (x: #x),
(#beta: _lvar_5),
(#v: _lvar_8),
(#wisl__0: l-nth(#x, 0i)),
(#wisl__1: l-nth(#x, 1i)),
(#z: _lvar_9) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(l+ ({{ _lvar_8 }}, _lvar_5) == l+ ({{ _lvar_8 }}, _lvar_5))
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Match MP: There are 1 states left to consider.
Substs:
[]
[_lvar_5, _lvar_8]
[]
Match assertion: types(alpha : List),
Subst:
[ (alpha: l+ ({{ _lvar_8 }}, _lvar_5)),
(x: #x),
(#beta: _lvar_5),
(#v: _lvar_8),
(#wisl__0: l-nth(#x, 0i)),
(#wisl__1: l-nth(#x, 1i)),
(#z: _lvar_9) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: (Lit 1i i+ (l-len _lvar_5)))
MEMORY:
_$l_1 -> BOUND: NONE
{}
PURE FORMULAE:
(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
PREDS:
WANDS:
VARIANTS:
llen,
Match MP: There are 1 states left to consider.
Matcher.match_mp: Matching successful: 1 states left
Matcher.match_: Success (possibly empty)
Out parameters : l+ ({{ _lvar_8 }}, _lvar_5)
Preds.consume_pred: Looking for: list[Some #x; Some #alpha]
Found 1 candidates:
[#x; l+ ({{ _lvar_8 }}, _lvar_5)]
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(l+ ({{ _lvar_8 }}, _lvar_5) == #alpha)
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Returning the following vs: #x, l+ ({{ _lvar_8 }}, _lvar_5)
learned the outs of a predicate. going to match (l+ ({{ _lvar_8 }}, _lvar_5)) against (
#alpha)!!!
Outs: []
Obtained values: [l+ ({{ _lvar_8 }}, _lvar_5)]
Obtained exprs: [#alpha]
Parameter subst
[ (0: l+ ({{ _lvar_8 }}, _lvar_5)) ]
Substed outs: []
Preparing entailment check:
Existentials:
Left:(#x == {{ _$l_1, _lvar_7 }})
(#alpha == l+ ({{ _lvar_8 }}, _lvar_5))
(0i i<=# (l-len #alpha))
(0i i<=# (l-len #x))
(0i i<=# (l-len _lvar_5))
Right:(l+ ({{ _lvar_8 }}, _lvar_5) == #alpha)
Gamma:
(#alpha: List)
(#x: List)
(_lvar_5: List)
(_lvar_7: Int)
REDUCED RPFS:
True
Finished existential simplification.
Existentials:
Left: (0i i<=# (l-len _lvar_5))
Right: True
Gamma:
(_lvar_5: List)
(_lvar_7: Int)
SAT check cached with result: false
Entailment returned true
Match MP: There are 1 states left to consider.
Matcher.match_mp: Matching successful: 1 states left
Matcher.match_: Success (possibly empty)
PSTATE.matches: Success: true
Analysis result: Postcondition matched successfully
VERIFICATION SUCCESS: Spec llen (0, 0) terminated successfully
-----------------------------------
STATE BEFORE SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(ret: Lit 1i)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
-----------------------------------
PFS/Gamma simplification:
With matching: No
PFS:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
Gamma:
(#alpha: List)
(#x: Null)
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
Gamma:
(#alpha: List)
(#x: Null)
Filtered and fixed subst, to be applied to memory:
[ ]
Substitution results in 1 results:
-----------------------------------
STATE AFTER SIMPLIFICATIONS:
SPEC VARS: #alpha, #x
STORE:
(ret: Lit 1i)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
with substitution:
[ ]
-----------------------------------
Analyse result: About to match one postcondition of llen. post: ┬À types(#alpha : List),
┬À (ret == (l-len #alpha)),
┬À list(#x, #alpha),
===FINISHED=== POST: None
Matcher.match_: about to match MP.
Match MP: There are 1 states left to consider.
Substs:
[]
[#alpha]
[]
Match assertion: types(#alpha : List),
Subst:
[ (ret: 1i), (#alpha: #alpha), (#x: #x) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: Lit 1i)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDS:
WANDS:
VARIANTS:
llen,
Match MP: There are 1 states left to consider.
Substs:
[]
[#alpha]
[]
Match assertion: (ret == (l-len #alpha)),
Subst:
[ (ret: 1i), (#alpha: #alpha), (#x: #x) ]
STATE:
SPEC VARS: #alpha, #x
STORE:
(ret: Lit 1i)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDS:
WANDS:
VARIANTS:
llen,
Preparing entailment check:
Existentials:
Left:(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
Right:(1i == (l-len #alpha))
Gamma:
(#alpha: List)
(#x: Null)
PFS/Gamma simplification:
With matching: No
PFS:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
Gamma:
(#alpha: List)
(#x: Null)
Analysing list structure.
Analysing list structure.
PFS/Gamma simplification completed:
PFS:
Gamma:
REDUCED RPFS:
False
Finished existential simplification.
Existentials:
Left:
Right: False
Gamma:
WARNING: Match Assertion Failed: (ret == (l-len #alpha)), with subst
[ (ret: 1i), (#alpha: #alpha), (#x: #x) ] in state
SPEC VARS: #alpha, #x
STORE:
(ret: Lit 1i)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDS:
WANDS:
VARIANTS:
llen,
with errors:
EAsrt(#alpha; (! (1i == (l-len #alpha))); [(1i == (l-len #alpha))])
Match MP: There are 0 states left to consider.
Can fix: (! (1i == (l-len #alpha))): true
Matcher.match_: Failure
Match. Unable to match. About to attempt the following recovery tactic:
{ "try_fold" = None;
"try_unfold" = Some [#alpha] }
Attempting to recover
No fold recovery tactic
Starting unfold_with_vals: #alpha
SPEC VARS: #alpha, #x
STORE:
(ret: Lit 1i)
MEMORY:
PURE FORMULAE:
(#x == null)
(#alpha == {{ }})
(0i i<=# (l-len #alpha))
TYPING ENVIRONMENT:
(#alpha: List)
(#x: Null)
PREDS:
WANDS:
VARIANTS:
llen,
.
NOTHING TO UNFOLD!!!!
Match. Recovery tactic failed: try_fold: None
try_unfold: Automatic unfold failed
PSTATE.matches: Success: false
Analysis result: Postcondition not matchable
VERIFICATION FAILURE: Spec llen (0, 0) - post condition not matchable
There were failures: 0.018922
Raw
llen.wisl
predicate list(+x, alpha) {
(x == null) * (alpha == nil);
(x -> #v, #z) * list(#z, #beta) * (alpha == #v::#beta)
}
{ (x == #x) * list(#x, #alpha) }
function llen(x) {
if (x = null) {
n := 1
} else {
t := [x+1];
n := llen(t);
n := n + 1
};
return n
}
{ list(#x, #alpha) * (ret == len(#alpha)) }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment