2.1.4.5 Insertion sort list

This version of insertion sort changes position of cells.

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
intlist insertSortLst(intlist x) {
  intlist xi, y, yi, z, r;
  z = xi = yi = y = NULL;
  r = z = x;
  xi = x->next;
  while (xi != NULL) {
    yi = NULL;
    y = r;
    while (y != xi && y->data < xi->data) {
      yi = y;
      y = y->next;
    }
    if (yi == NULL) {
      z->next = xi->next;
      xi->next = r;
      r = xi;
    }
    else {
      z->next = xi->next;
      yi->next = xi;
      xi->next = y;
    }
    xi = NULL;
    xi = z->next;
  }
  return r;
}


var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, xip:real, y:real, yp:real, z:real,
    _l:int, _k:int, S:int;
begin
  assume (x == 0); 
  xi = _null; y = _null;
  xip = _null; yp = _null; z = _null;
  xip = x;
  xi = x * _next;
  while xi != _null do
    y = x;
    while y != xi and y * _data <= xi * _data do
      yp = _null;
      yp = y;
      z = y * _next;
      y = _null;
      y = z;
      z = _null;
    done;
    if y != xi then
      xip = _null / _next;
      z = xi * _next;
      xip = z / _next;
      z = _null;
      if yp == _null then
        xi = _null / _next;
        xi = x / _next;
        x = _null;
        x = xi;
      else
        yp = _null / _next;
        yp = xi / _next;
        xi = _null / _next;
        xi = y / _next;
        yp = _null;
      endif;
      y = _null;
      xi = _null;
    else
      xip = _null;
      xip = xi;
      yp = _null;
      y = _null;
      xi = _null;
    endif;
    xi = xip * _next;
  done;
end

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
TODO
TODO
TODO

LSUM-REL
TODO
TODO
TODO

MSET
TODO
TODO
TODO

UCONS
TODO
TODO
TODO