default Order dec

$include <exception_basic.sail>
$include <flow.sail>
$include <vector_dec.sail>
$include <arith.sail>

function main (() : unit) -> unit = {
  assert(sub_int(0, 0) == 0);
  assert(sub_int(0, 14) == -14);
  assert(sub_int(0, 17) == -17);
  assert(sub_int(0, 29) == -29);
  assert(sub_int(0, 30) == -30);
  assert(sub_int(0, 33) == -33);
  assert(sub_int(0, 38) == -38);
  assert(sub_int(0, 52) == -52);
  assert(sub_int(0, 56) == -56);
  assert(sub_int(1, 0) == 1);
  assert(sub_int(1, 1) == 0);
  assert(sub_int(1, 14) == -13);
  assert(sub_int(1, 30) == -29);
  assert(sub_int(1, 5) == -4);
  assert(sub_int(1, 50) == -49);
  assert(sub_int(10, 10) == 0);
  assert(sub_int(10, 13) == -3);
  assert(sub_int(10, 17) == -7);
  assert(sub_int(10, 9) == 1);
  assert(sub_int(100, 64) == 36);
  assert(sub_int(1024, 1) == 1023);
  assert(sub_int(11, 1) == 10);
  assert(sub_int(11, 10) == 1);
  assert(sub_int(11, 11) == 0);
  assert(sub_int(11, 14) == -3);
  assert(sub_int(11, 21) == -10);
  assert(sub_int(11, 30) == -19);
  assert(sub_int(111, 64) == 47);
  assert(sub_int(12, 1) == 11);
  assert(sub_int(12, 10) == 2);
  assert(sub_int(12, 14) == -2);
  assert(sub_int(128, 128) == 0);
  assert(sub_int(13, 10) == 3);
  assert(sub_int(13, 3) == 10);
  assert(sub_int(13, 59) == -46);
  assert(sub_int(14, 0) == 14);
  assert(sub_int(14, 1) == 13);
  assert(sub_int(14, 10) == 4);
  assert(sub_int(14, 26) == -12);
  assert(sub_int(14, 3) == 11);
  assert(sub_int(14, 59) == -45);
  assert(sub_int(14, 8) == 6);
  assert(sub_int(15, 0) == 15);
  assert(sub_int(15, 10) == 5);
  assert(sub_int(15, 16) == -1);
  assert(sub_int(16, 1) == 15);
  assert(sub_int(16, 10) == 6);
  assert(sub_int(16, 22) == -6);
  assert(sub_int(16, 36) == -20);
  assert(sub_int(17, 10) == 7);
  assert(sub_int(17, 22) == -5);
  assert(sub_int(17, 40) == -23);
  assert(sub_int(17, 62) == -45);
  assert(sub_int(18, 10) == 8);
  assert(sub_int(18, 11) == 7);
  assert(sub_int(18, 19) == -1);
  assert(sub_int(18, 24) == -6);
  assert(sub_int(19, 10) == 9);
  assert(sub_int(2, 0) == 2);
  assert(sub_int(2, 2) == 0);
  assert(sub_int(2, 5) == -3);
  assert(sub_int(20, 20) == 0);
  assert(sub_int(21, 1) == 20);
  assert(sub_int(21, 18) == 3);
  assert(sub_int(21, 2) == 19);
  assert(sub_int(21, 20) == 1);
  assert(sub_int(22, 10) == 12);
  assert(sub_int(22, 20) == 2);
  assert(sub_int(23, 11) == 12);
  assert(sub_int(23, 20) == 3);
  assert(sub_int(23, 39) == -16);
  assert(sub_int(24, 1) == 23);
  assert(sub_int(24, 14) == 10);
  assert(sub_int(24, 20) == 4);
  assert(sub_int(24, 25) == -1);
  assert(sub_int(24, 62) == -38);
  assert(sub_int(25, 1) == 24);
  assert(sub_int(25, 10) == 15);
  assert(sub_int(25, 20) == 5);
  assert(sub_int(25, 45) == -20);
  assert(sub_int(256, 1) == 255);
  assert(sub_int(26, 1) == 25);
  assert(sub_int(26, 20) == 6);
  assert(sub_int(26, 27) == -1);
  assert(sub_int(27, 20) == 7);
  assert(sub_int(27, 22) == 5);
  assert(sub_int(27, 3) == 24);
  assert(sub_int(27, 56) == -29);
  assert(sub_int(27, 59) == -32);
  assert(sub_int(28, 1) == 27);
  assert(sub_int(28, 15) == 13);
  assert(sub_int(28, 16) == 12);
  assert(sub_int(28, 20) == 8);
  assert(sub_int(28, 8) == 20);
  assert(sub_int(29, 20) == 9);
  assert(sub_int(29, 6) == 23);
  assert(sub_int(3, 0) == 3);
  assert(sub_int(3, 1) == 2);
  assert(sub_int(3, 2) == 1);
  assert(sub_int(3, 3) == 0);
  assert(sub_int(3, 44) == -41);
  assert(sub_int(3, 62) == -59);
  assert(sub_int(30, 30) == 0);
  assert(sub_int(31, 0) == 31);
  assert(sub_int(31, 16) == 15);
  assert(sub_int(31, 24) == 7);
  assert(sub_int(31, 26) == 5);
  assert(sub_int(31, 30) == 1);
  assert(sub_int(31, 8) == 23);
  assert(sub_int(32, 1) == 31);
  assert(sub_int(32, 11) == 21);
  assert(sub_int(32, 12) == 20);
  assert(sub_int(32, 16) == 16);
  assert(sub_int(32, 24) == 8);
  assert(sub_int(32, 26) == 6);
  assert(sub_int(32, 32) == 0);
  assert(sub_int(32, 53) == -21);
  assert(sub_int(32, 7) == 25);
  assert(sub_int(32, 8) == 24);
  assert(sub_int(33, 1) == 32);
  assert(sub_int(33, 39) == -6);
  assert(sub_int(34, 1) == 33);
  assert(sub_int(35, 0) == 35);
  assert(sub_int(35, 1) == 34);
  assert(sub_int(35, 25) == 10);
  assert(sub_int(35, 36) == -1);
  assert(sub_int(35, 48) == -13);
  assert(sub_int(36, 1) == 35);
  assert(sub_int(36, 10) == 26);
  assert(sub_int(36, 59) == -23);
  assert(sub_int(39, 32) == 7);
  assert(sub_int(4, 0) == 4);
  assert(sub_int(4, 1) == 3);
  assert(sub_int(4, 2) == 2);
  assert(sub_int(4, 4) == 0);
  assert(sub_int(4, 5) == -1);
  assert(sub_int(4, 54) == -50);
  assert(sub_int(4, 7) == -3);
  assert(sub_int(4, 9) == -5);
  assert(sub_int(40, 28) == 12);
  assert(sub_int(40, 32) == 8);
  assert(sub_int(42, 22) == 20);
  assert(sub_int(42, 39) == 3);
  assert(sub_int(42, 54) == -12);
  assert(sub_int(43, 29) == 14);
  assert(sub_int(43, 32) == 11);
  assert(sub_int(44, 34) == 10);
  assert(sub_int(45, 19) == 26);
  assert(sub_int(46, 36) == 10);
  assert(sub_int(46, 61) == -15);
  assert(sub_int(47, 0) == 47);
  assert(sub_int(47, 1) == 46);
  assert(sub_int(47, 15) == 32);
  assert(sub_int(47, 47) == 0);
  assert(sub_int(48, 1) == 47);
  assert(sub_int(48, 14) == 34);
  assert(sub_int(48, 32) == 16);
  assert(sub_int(48, 47) == 1);
  assert(sub_int(49, 6) == 43);
  assert(sub_int(5, 0) == 5);
  assert(sub_int(5, 11) == -6);
  assert(sub_int(5, 14) == -9);
  assert(sub_int(5, 2) == 3);
  assert(sub_int(5, 7) == -2);
  assert(sub_int(51, 47) == 4);
  assert(sub_int(51, 5) == 46);
  assert(sub_int(51, 63) == -12);
  assert(sub_int(52, 14) == 38);
  assert(sub_int(52, 4) == 48);
  assert(sub_int(52, 48) == 4);
  assert(sub_int(52, 59) == -7);
  assert(sub_int(54, 34) == 20);
  assert(sub_int(54, 47) == 7);
  assert(sub_int(55, 60) == -5);
  assert(sub_int(55, 7) == 48);
  assert(sub_int(56, 12) == 44);
  assert(sub_int(56, 32) == 24);
  assert(sub_int(56, 52) == 4);
  assert(sub_int(57, 12) == 45);
  assert(sub_int(58, 32) == 26);
  assert(sub_int(58, 34) == 24);
  assert(sub_int(58, 62) == -4);
  assert(sub_int(59, 60) == -1);
  assert(sub_int(6, 0) == 6);
  assert(sub_int(6, 1) == 5);
  assert(sub_int(6, 10) == -4);
  assert(sub_int(6, 2) == 4);
  assert(sub_int(6, 3) == 3);
  assert(sub_int(6, 33) == -27);
  assert(sub_int(6, 4) == 2);
  assert(sub_int(6, 5) == 1);
  assert(sub_int(6, 6) == 0);
  assert(sub_int(6, 7) == -1);
  assert(sub_int(61, 13) == 48);
  assert(sub_int(62, 31) == 31);
  assert(sub_int(62, 56) == 6);
  assert(sub_int(62, 63) == -1);
  assert(sub_int(63, 14) == 49);
  assert(sub_int(63, 48) == 15);
  assert(sub_int(64, 0) == 64);
  assert(sub_int(64, 1) == 63);
  assert(sub_int(64, 12) == 52);
  assert(sub_int(64, 14) == 50);
  assert(sub_int(64, 16) == 48);
  assert(sub_int(64, 2) == 62);
  assert(sub_int(64, 21) == 43);
  assert(sub_int(64, 24) == 40);
  assert(sub_int(64, 28) == 36);
  assert(sub_int(64, 3) == 61);
  assert(sub_int(64, 32) == 32);
  assert(sub_int(64, 33) == 31);
  assert(sub_int(64, 34) == 30);
  assert(sub_int(64, 35) == 29);
  assert(sub_int(64, 36) == 28);
  assert(sub_int(64, 39) == 25);
  assert(sub_int(64, 52) == 12);
  assert(sub_int(64, 64) == 0);
  assert(sub_int(64, 7) == 57);
  assert(sub_int(64, 8) == 56);
  assert(sub_int(64, 9) == 55);
  assert(sub_int(68, 64) == 4);
  assert(sub_int(7, 0) == 7);
  assert(sub_int(7, 1) == 6);
  assert(sub_int(7, 19) == -12);
  assert(sub_int(7, 34) == -27);
  assert(sub_int(7, 41) == -34);
  assert(sub_int(72, 64) == 8);
  assert(sub_int(76, 64) == 12);
  assert(sub_int(78, 64) == 14);
  assert(sub_int(8, 0) == 8);
  assert(sub_int(8, 1) == 7);
  assert(sub_int(8, 16) == -8);
  assert(sub_int(8, 19) == -11);
  assert(sub_int(8, 26) == -18);
  assert(sub_int(89, 64) == 25);
  assert(sub_int(9, 0) == 9);
  assert(sub_int(9, 1) == 8);
  assert(sub_int(9, 13) == -4);
  assert(sub_int(9, 6) == 3);
  assert(sub_int(9, 8) == 1);
}