2.1.3.4 Add some constant

C code 
Spl encoding

#include "intlist.h"

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


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

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,1)
log/intlist-add2-lsum-prd-01
x(n1) and S[n1]>=S+2

LSUM-REL
Anon=(0,1)
log/intlist-add2-lsum-rel-01
x(n1) and S[n1]=S+2*l[n1]

MSET


none

UCONS
Anon=(0,1)
TODO
x(n1)