2.1.3.2 Copy the list data to a different length list (correct)

This example is the correct version of copying lists of different lengths. The only interesting part is that the bug detected for the next example is not found here.

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) and
 * acyclic(y) and l[y]+1<=_l and data(y) and
 * disjoint(x,y) */
void listCopy(intlist x, intlist y) {
  intlist xi = x;
  intlist yi = y;
  while (xi != NULL && yi != NULL) {
    yi->data = xi->data;
    xi = xi->next;
    yi = yi->next;
  }
}


var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, y:real, yi:real, z:real,
    _l:int, _k:int, S: int;
begin
  assume (x == 3);
  xi = _null; yi = _null; z = _null;
  xi = x; yi = y;
  while xi != _null and yi != _null do
    yi = (xi* _data) / _data;
    z = xi*_next;
    xi = _null;
    xi = z;
    z = _null;
    z = yi*_next;
    yi = _null;
    yi = z;
    z = _null;
  done;
end

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,1)
log/intlist-copy-neq-lsum-prd-01
x(n1) and xi(n2) and y(n3) and yi=null
and d(n1)=d(n3) and S(n1) = S(n3)

LSUM-REL
Anon=(0,1)
log/intlist-copy-neq-lsum-rel-01
x(n1) and xi(n2) and y(n3) and yi=null
and d(n1)=d(n3) and S(n1) = S(n3)

MSET
TODO
TODO
TODO

UCONS
TODO
TODO
x(n1) and xi(n2) and y(n3) and yi=null and
and d(n1)=d(n3) and \forall y1\in n1, y2\in n2. y1=y2 \implies d(y1)=d(y2)