2.1.4.2 New copy and add of a list

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
intlist add2new(intlist x) {
  intlist xi = x;
  intlist yi, y, z;
  yi = y = z = NULL;
  while (xi != NULL) {
    z = new();
    z->data = xi->data + 2;
    if (yi == NULL)
      y = z;
    else {
      yi->next = z;
      yi = NULL;
    }
    yi = z;
    z = NULL;
    xi = xi->next;
  }
  return y;
}


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 == 0);
  y = _null;
  yi = _null;
  z = _null;
  xi = _null;
  xi = x;
  while xi != _null do
    z = _new;
    z = (xi * _data + 2) / _data;
    z = _null / _next;
    if (yi == _null) then
      y = z;
    else
      yi = _null/_next;
      yi = z/_next;
    endif;
    yi = _null;
    yi = z;
    z = _null;
    z = xi * _next;
    xi = _null;
    xi = z;
    z = _null;
  done;
end

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,1)
log/intlist-add2new-lsum-prd-01
x(n1) and y(n2) and yi(n3) and
l[n1]=l[n2]+1 and l[n3]=1 and
d(n2)=d(n1)+2 and
S[n3]=0 and S[n2]+d(n3)>=S+2 and S=S[n1]

LSUM-REL
Anon=(0,1)
log/intlist-add2new-lsum-rel-01
x(n1) and y(n2) and yi(n3) and
l=l[n1]=l[n2]+1 and l[n3]=1 and
d(n2)=d(n1)+2 and
S[n3]=0 and S[n2]+d(n3)+2=S+2l and S[n1]=S

MSET


none

UCONS
Anon=(0,2)
TODO
x(n1) and y(n2) and yi(n3) and
l=l[n1]=l[n2]+1 and l[n3]=1 and
d(n1)=d(n2) and
\forall y1\in n1, y2\in n2. y1=y2 \implies d(y1)=d(y2)