2.1.3.6 Copy a list and add some constant for different length lists (correct)

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 add2copy_neq(intlist x, intlist y) {
  intlist xi = x;
  intlist yi = y;
  while (xi != NULL && yi != NULL) {
    yi->data = xi->data + 2;
    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, z1:real, z2:real,
    _l:int, _k: int, S: int;
begin
  assume (x == 3);
  xi = _null; yi = _null; z1 = _null; z2 = _null;
  xi = x;
  yi = y;
  while xi != _null and yi != _null do
    yi = (xi * _data + 2)/ _data;
    z1 = xi* _next;
    z2 = yi* _next;
    xi = _null; yi = _null;
    xi = z1; yi = z2;
    z1 = _null; z2 = _null;
  done;
end

Results

Domain 
Param. 
Log file 
Interesting constraint

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

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

MSET


none

UCONS
Anon=(0,2)
TODO
x(n1) and y(n2) and
\forall y1\in n1, y2\in n2 y1=y2 \implies d(y2)=d(y1)+2