2.1.3.7 Set the flag

C code 
Spl encoding

#include "intlist.h"

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


var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, z:real,
    _l:int, _k:int, S: int;
begin
 assume (x == 0); 
 xi = _null; z = _null;
 xi = x;
 while xi != _null do
    if (xi* _data == 0) then
      xi = 1 / _data;
    endif;
    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-setFlag-lsum-prd-01
x(n1) and
S(n1)+d(n1) >= S

LSUM-REL
Anon=(0,1)
log/intlist-setFlag-lsum-rel-01
x(n1) and
S(n1)+d(n1) >= S and S(n1)+d(n1) <= S+l[n1]

MSET
TODO
TODO
x(n1) and M[n1]=M-\0\+\1\

UCONS
Anon=(0,1)
TODO
x(n1) and \forall y1\in n1 \implies d(y1)!=0