2.1.1.5 Sum of elements

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x)  */
int listSum(intlist x) {
  intlist xi = x;
  int sum = 0;
  while (xi != NULL) {
    sum = sum + xi->data; 
    xi = xi->next;
  }
  return sum;
}


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, sum:int;
begin
  assume (x == 0); 
  xi = _null; y = _null;
  xi = x;
  sum = 0;
  while xi != _null do
    sum = sum + xi * _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-sum-lsum-prd-01/
x(n1) and l=l[n1] and S=S[n1]=v


LSUM-REL
Anon=(0,1)
log/intlist-sum-lsum-rel-01/
same as above


MSET

TODO
x(n1) and l=l[n1] and M[n1]=M


UCONS
Anon=(0,1)
TODO
x(n1) and l=l[n1]