2.1.2.3 Initialization with first even numbers

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
void init2N(intlist x) {
  intlist xi = x;
  int m = 0;
  while (xi != NULL) {
    xi->data = m;
    xi = xi->next;
    m = m+2;
  }
}


var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, z:real,
    _l:int, _k: int, m:int;
begin
  assume (x == 0); 
  xi = _null; z = _null;
  m = 2;
  xi = x;
  while xi != _null do
    xi = m / _data;
    z = xi*_next;
    xi = _null;
    xi = z;
    z = _null;
    m = m+2;
  done;
end

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,1)
log/intlist-init2N-lsum-prd-01
x(n1) and d(n1)=0


LSUM-REL
Anon=(0,1)
log/intlist-init2N-lsum-rel-01
x(n1) and 2l(n1)=m and d(n1)=0 and _l=l[n1]


LSUM-REL
Anon=(0,1)
TODO
with grid constraints


MSET


none


UCONS
Anon=(0,1) or (2,1),
P11 or P211
TODO
x(n1)
and \forall y \in n1 \implies d(y)=2y
and \forall y1 <_1 y2 \in n1 \implies d(y2)=d(y1)+2