2.1.2.6 Partial reset

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and 
 * l[x]+l[y]==_l and data(xy) and
 * reach(x,y) */
void partialInit(intlist x, 
                 intlist y) {
  intlist yi = y;
  while (yi != NULL) {
    yi->data = 0;
    yi = yi->next;
  }
}


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

Results

Domain 
Param. 
Log file 
Interesting constraint

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

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

MSET
TODO
TODO
TODO

UCONS
TODO
TODO
x(n1) and y(n2)
and \forall y1\in n2 \implies d(y1)=0