From f8eaa5a7a5088789bae805f1d544f23f06efdb29 Mon Sep 17 00:00:00 2001 From: Aurelien Rebourg Date: Thu, 16 Jan 2020 17:02:40 +0100 Subject: [PATCH] scalable debut --- .gitignore | 5 +- .../tests/test_builtin_generate_primes.ml | 2 +- Source/scalable/scalable.ml | 252 +- Source/scalable/tests/test_scalable.ml | 2883 +++++++++++++++++ .../scalable/tests/test_scalable_ciphers.ml | 4 +- 5 files changed, 3112 insertions(+), 34 deletions(-) diff --git a/.gitignore b/.gitignore index 15aff4c..526c318 100644 --- a/.gitignore +++ b/.gitignore @@ -31,6 +31,7 @@ _opam/ # Local files *~ +# Log files + *.log -*.cache -*caml-toplevel* +*.cache \ No newline at end of file diff --git a/Source/builtin/tests/test_builtin_generate_primes.ml b/Source/builtin/tests/test_builtin_generate_primes.ml index 6be78ae..6b6c39f 100644 --- a/Source/builtin/tests/test_builtin_generate_primes.ml +++ b/Source/builtin/tests/test_builtin_generate_primes.ml @@ -26,7 +26,7 @@ let () = let t_list = [((20, is_prime), [(2, 5); (3, 7); (5, 11); (11, 23)])] run_test template_1f_L2 "Double Primes Generator" double_primes t_list ;; -let () = let t_list = [((20, is_prime), [(2, 3); (3, 5); (5, 7); (11, 13); (17, 19)])] +let () = let t_list = [((20, is_prime), [(3, 5); (5, 7); (11, 13); (17, 19)])] in run_test template_1f_L2 "Twin Primes Generator" twin_primes t_list ;; diff --git a/Source/scalable/scalable.ml b/Source/scalable/scalable.ml index 522de05..343ef82 100644 --- a/Source/scalable/scalable.ml +++ b/Source/scalable/scalable.ml @@ -1,3 +1,4 @@ + (** A naive implementation of big integers This module aims at creating a set of big integers naively. Such data @@ -17,19 +18,82 @@ decomposition of a non-negative integer. (** Creates a bitarray from a built-in integer. @param x built-in integer. *) -let from_int x = [] +let sign x = + if x < 0 then + -1 + else + 1;; + + +let from_int x = + if x = 0 then [] + else + let rec from_int_rec n = + match n with + 0 -> [] + | n -> n mod 2::from_int_rec (n/2) + in let bitsign = + if sign x = -1 then + 1 + else + 0 + in bitsign::from_int_rec (sign x * x);; (** Transforms bitarray of built-in size to built-in integer. UNSAFE: possible integer overflow. @param bA bitarray object. - *) -let to_int bA = 0 +*) + +let modulo a b = + match sign a = -1 && a mod b != 0 with + true -> a mod b + b + | _ -> a mod b;; + +let power x n = + if n = 0 then 1 else + let rec power_rec x1 n = + match n with + 1 -> x1 + | n when modulo n 2 = 0 -> power_rec (x1 * x1) (n/2) + | n -> x1 * power_rec (x1 * x1) ((n-1)/2) + in power_rec x n;; + + +let to_int bA = + match bA with + [] -> 0 + | e::bA1 -> begin + let sign = match e with + 0 -> 1 + | _ -> -1 + in let rec to_int_rec bA pow = + match bA with + [] -> 0 + | e::bA1 -> (e * power 2 pow) + to_int_rec bA1 (pow + 1) + in sign * to_int_rec bA1 0 + end;; (** Prints bitarray as binary number on standard output. @param bA a bitarray. *) -let print_b bA = () - +let print_b bA = + match bA with + [] -> print_endline "0" + | e::l1 -> begin + let rec print_b_rec bA = + match bA with + [] -> print_endline "" + | e::l1 -> begin + print_b_rec l1; + print_int e + end + in + if e = 1 then ( + print_string "-"; + print_b_rec l1 + ) else + print_b_rec l1 + end;; (** Toplevel directive to use print_b as bitarray printer. CAREFUL: print_b is then list int printer. UNCOMMENT FOR TOPLEVEL USE. @@ -46,22 +110,45 @@ let print_b bA = () @param nA A natural, a bitarray having no sign bit. Assumed non-negative. @param nB A natural. - *) -let rec compare_n nA nB = 0 +*) + +let rec rem_0 bA = + match bA with + [] -> [] + | 1::l1 -> 1::l1 + | _::l1 -> rem_0 l1;; + + +let compare_n nA nB = + let nA = rem_0 (List.rev nA) + and nB = rem_0 (List.rev nB) + in if List.length nA > List.length nB then + 1 + else if List.length nA < List.length nB then + -1 + else + let rec compare_n_rec nA nB = + match (nA, nB) with + ([], []) -> 0 + | ([], _) | (0::_, 1::_) -> -1 + | (_, []) | (1::_, 0::_) -> 1 + | (_::l1, _::l2) -> compare_n_rec l1 l2 + in compare_n_rec nA nB;; + (** Bigger inorder comparison operator on naturals. Returns true if first argument is bigger than second and false otherwise. @param nA natural. @param nB natural. *) -let (>>!) nA nB = true +let (>>!) nA nB = compare_n nA nB = 1;; (** Smaller inorder comparison operator on naturals. Returns true if first argument is smaller than second and false otherwise. @param nA natural. @param nB natural. *) -let (<=!) nA nB = true +let (>=!) nA nB = compare_n nA nB = 1 || compare_n nA nB = 0;; (** Smaller or equal inorder comparison operator on naturals. Returns true if first argument is smaller or equal to second and false @@ -77,28 +164,36 @@ let (>=!) nA nB = true @param nA natural. @param nB natural. *) -let (<=!) nA nB = true +let (<=!) nA nB = compare_n nA nB = -1 || compare_n nA nB = 0;; (** Comparing two bitarrays. Output is 1 if first argument is bigger than second -1 if it smaller and 0 in case of equality. @param bA A bitarray. @param bB A bitarray. *) -let compare_b bA bB = 0 +let compare_b bA bB = + match (bA, bB) with + ([], []) -> 0 + | ([], _) | (1::_, 0::_) -> -1 + | (_, []) | (0::_, 1::_) -> 1 + | (sign:: nA, _::nB) -> + match sign with + 0 -> compare_n (0::nA) (0::nB) + | _ -> -1 * compare_n (0::nA) (0::nB);; (** Bigger inorder comparison operator on bitarrays. Returns true if first argument is bigger than second and false otherwise. @param nA natural. @param nB natural. *) -let (<<) bA bB = true +let (<<) bA bB = compare_b bA bB = -1;; (** Smaller inorder comparison operator on bitarrays. Returns true if first argument is smaller than second and false otherwise. @param nA natural. @param nB natural. *) -let (>>) bA bB = true +let (>>) bA bB = compare_b bA bB = 1;; (** Bigger or equal inorder comparison operator on bitarrays. Returns true if first argument is bigger or equal to second and false @@ -106,7 +201,7 @@ let (>>) bA bB = true @param nA natural. @param nB natural. *) -let (<<=) bA bB = true +let (<<=) bA bB = compare_b bA bB = -1 || compare_b bA bB = 0;; (** Smaller or equal inorder comparison operator on naturals. Returns true if first argument is smaller or equal to second and false @@ -114,52 +209,122 @@ let (<<=) bA bB = true @param nA natural. @param nB natural. *) -let (>>=) bA bB = true -;; +let (>>=) bA bB = compare_b bA bB = 1 || compare_b bA bB = 0;; (** Sign of a bitarray. @param bA Bitarray. *) -let sign_b bA = 0 +let sign_b bA = + match bA with + [] -> 1 + | e::_ when e = 1 -> -1 + | _ -> 1;; (** Absolute value of bitarray. @param bA Bitarray. *) -let abs_b bA = [] +let abs_b bA = + match bA with + [] -> [] + | _::bA -> 0::bA;; (** Quotient of integers smaller than 4 by 2. @param a Built-in integer smaller than 4. *) -let _quot_t a = 0 +let _quot_t a = + match a with + 0 | 1-> 0 + | 2 | 3-> 1 + | _ -> invalid_arg "must be smaller than 4";; (** Modulo of integer smaller than 4 by 2. @param a Built-in integer smaller than 4. *) -let _mod_t a = 0 +let _mod_t a = + match a with + 0 | 2-> 0 + | 1 | 3-> 1 + | _ -> invalid_arg "must be smaller than 4";; (** Division of integer smaller than 4 by 2. @param a Built-in integer smaller than 4. *) -let _div_t a = (0, 0) +let _div_t a = (_quot_t a, _mod_t a);; (** Addition of two naturals. @param nA Natural. @param nB Natural. *) -let add_n nA nB = [] +let add_n nA nB = + match (nA, nB) with + (l, []) | ([], l) -> l + | (_::nA, _::nB) -> + let rec add_n_rec nA nB ret res= + match (nA, nB) with + ([], []) -> ret::res + | (e::l1, []) | ([], e::l1) -> let tot = e + ret in + let (q, r) = _div_t tot in + add_n_rec l1 [] q (r::res) + | (e1::nA, e2::nB) -> + let tot = e1 + e2 + ret in + let (q, r) = _div_t tot in + add_n_rec nA nB q (r::res) + in List.rev (add_n_rec nA nB 0 [0]);; + (** Difference of two naturals. UNSAFE: First entry is assumed to be bigger than second. @param nA Natural. @param nB Natural. *) -let diff_n nA nB = [] +let bit_comp = function 0 -> 1 | _ -> 0;; + + +let complem2 bA n= + match bA with + [] -> [] + | e::bA -> + let rec complem_rec bA comp res n= + match n with + 0 -> res + | n -> + let (e:: bA) = match bA with + [] -> [0] + | _ -> bA in + let res = if comp then + (bit_comp e)::res + else e::res + and comp = if not comp && e = 1 then true else comp + in complem_rec bA comp res (n-1) + in bit_comp e::List.rev (complem_rec bA false [] (n - 1));; + +let diff_n nA nB = add_n nA (complem2 nB (List.length nA)) (** Addition of two bitarrays. @param bA Bitarray. @param bB Bitarray. - *) -let add_b bA bB = [] +*) + +let get_signed_bitarray bsign bA = + match bA with + [] -> [] + | _::bA -> bsign::bA;; + +let add_b bA bB = + match (bA, bB) with + ([], l) | (l, []) -> l + | (0::bA, 0::bB) -> get_signed_bitarray 0 (add_n (0::bA) (0::bB)) + | (1::bA, 1::bB) -> get_signed_bitarray 1 (add_n (0::bA) (0::bB)) + | (1::bA, 0::bB) when (<<=) (0::bA) (0::bB) -> + get_signed_bitarray 0 (diff_n (0::bB) (0::bA)) + | (1::bA, 0::bB) -> + get_signed_bitarray 1 (add_n (0::bB) (complem2 (1::bA) (List.length bA))) + | (0::bA, 1::bB) when (<<) (0::bA) (0::bB) -> + get_signed_bitarray 1 (add_n (0::bA) (complem2 (1::bB) (List.length bB))) + | (0::bA, 1::bB) -> + get_signed_bitarray 0 (diff_n (0::bA) (0::bB)) + | _ -> failwith "error" + (** Difference of two bitarrays. @param bA Bitarray. @@ -171,19 +336,48 @@ let diff_b bA bB = [] @param bA Bitarray. @param d Non-negative integer. *) -let rec shift bA d = [] +let rec shift bA d = + match d with + 0 -> bA + | d -> 0::shift bA (d-1);; (** Multiplication of two bitarrays. @param bA Bitarray. @param bB Bitarray. *) -let mult_b bA bB = [] +let mult_b bA bB = + match (bA, bB) with + ([], _) | (_, []) -> [] + | (sign1::bA, sign2::bB) -> + let rec mult_b_rec bA bB n = + match bA with + [] -> [] + | e::bA -> + let a = match e with 0 -> [] | 1 -> bB in + add_n (shift a n) (mult_b_rec bA bB (n+1)) + in match (sign1, sign2) with + (0,0) | (1,1) -> 0::mult_b_rec bA bB 0 + | _ -> 1::mult_b_rec bA bB 0 (** Quotient of two bitarrays. @param bA Bitarray you want to divide by second argument. @param bB Bitarray you divide by. Non-zero! *) -let quot_b bA bB = [] +let quot_b bA bB = + match (bA, bB) with + ([], _) | (_, []) -> [] + | (sign1::bA, sign2::bB) -> + let rec quot_b_rec bA bB n = + match bA with + [] -> [] + | e::bA -> + let a = match e with 0 -> [] | 1 -> bB in + add_n (shift a n) (quot_b_rec bA bB (n+1)) + in match (sign1, sign2) with + (0,0) | (1,1) -> 0::mult_b_rec bA bB 0 + | _ -> 1::mult_b_rec bA bB 0 + + (** Modulo of a bitarray against a positive one. @param bA Bitarray the modulo of which you're computing. diff --git a/Source/scalable/tests/test_scalable.ml b/Source/scalable/tests/test_scalable.ml index e69de29..6f0bb8e 100644 --- a/Source/scalable/tests/test_scalable.ml +++ b/Source/scalable/tests/test_scalable.ml @@ -0,0 +1,2883 @@ +open OUnit2 +open Scalable +open Test_scalable_templates + + +(* + Hi, this tests have been written by Paul Beaubois from Eng1. + They come with absolutly no garanty. + Use them wisely. +*) + + + + +let format_11i out_c (x, y) = + Printf.sprintf "(%i, %i)" (to_int x) y + +(* Personnal template *) +let my_format_1_1L out_c (a, b) = + Printf.sprintf "(%i, %i)" a (to_int b) +let format_2_1i out_c (x_2, t) = + Printf.sprintf "(%a, %i)" format_2 x_2 t +let format_11i_1 out_c (x_2, t) = + Printf.sprintf "(%a, %i)" format_11i x_2 (to_int t) + +let my_o_printer_1L a = Printf.sprintf "%i" (to_int a) +let o_printer_1i i = Printf.sprintf "%i" i + +let my_template_1_1L = template my_format_1_1L det_1 my_o_printer_1L +let template_2_1i = template format_2_1i det_2 o_printer_1i +let template_11i_1 = template format_11i_1 det_2 my_o_printer_1L + +(* Personnal tests *) + +let () = + let t_list = + [(11, [0; 1; 1; 0; 1]); (-11, [1; 1; 1; 0; 1]); (0, []); + (-1, [1; 1]); (1, [0; 1])] + in + run_test my_template_1_1L "from_int" from_int t_list +;; + +let () = + let t_list = + [(from_int 32, from_int 6), 1; + (from_int 18, from_int 12), 1; + (from_int (-18), from_int (-12)), -1; + (from_int (-11), from_int (-12)), 1; + (from_int (18), from_int (-12)), 1; + (from_int (-18), from_int (12)), -1; + (from_int (-18), from_int (-18)), 0; + ] + in + run_test template_2_1i "compare_b" compare_b t_list +;; + +let () = + let t_list = + [ + (from_int (0), from_int (0)), from_int (0); + (from_int (0), from_int (1)), from_int (1); + (from_int (0), from_int (2)), from_int (2); + (from_int (0), from_int (3)), from_int (3); + (from_int (0), from_int (4)), from_int (4); + (from_int (0), from_int (5)), from_int (5); + (from_int (0), from_int (515)), from_int (515); + (from_int (0), from_int (7)), from_int (7); + (from_int (0), from_int (9)), from_int (9); + (from_int (0), from_int (11)), from_int (11); + (from_int (0), from_int (13)), from_int (13); + (from_int (0), from_int (16)), from_int (16); + (from_int (0), from_int (17)), from_int (17); + (from_int (0), from_int (19)), from_int (19); + (from_int (0), from_int (23)), from_int (23); + (from_int (0), from_int (25)), from_int (25); + (from_int (0), from_int (29)), from_int (29); + (from_int (0), from_int (5026)), from_int (5026); + (from_int (0), from_int (5489)), from_int (5489); + (from_int (0), from_int (-1)), from_int (-1); + (from_int (0), from_int (-5)), from_int (-5); + (from_int (0), from_int (-4)), from_int (-4); + (from_int (0), from_int (-3)), from_int (-3); + (from_int (0), from_int (-2)), from_int (-2); + (from_int (1), from_int (0)), from_int (1); + (from_int (1), from_int (1)), from_int (2); + (from_int (1), from_int (2)), from_int (3); + (from_int (1), from_int (3)), from_int (4); + (from_int (1), from_int (4)), from_int (5); + (from_int (1), from_int (5)), from_int (6); + (from_int (1), from_int (515)), from_int (516); + (from_int (1), from_int (7)), from_int (8); + (from_int (1), from_int (9)), from_int (10); + (from_int (1), from_int (11)), from_int (12); + (from_int (1), from_int (13)), from_int (14); + (from_int (1), from_int (16)), from_int (17); + (from_int (1), from_int (17)), from_int (18); + (from_int (1), from_int (19)), from_int (20); + (from_int (1), from_int (23)), from_int (24); + (from_int (1), from_int (25)), from_int (26); + (from_int (1), from_int (29)), from_int (30); + (from_int (1), from_int (5026)), from_int (5027); + (from_int (1), from_int (5489)), from_int (5490); + (from_int (1), from_int (-1)), from_int (0); + (from_int (1), from_int (-5)), from_int (-4); + (from_int (1), from_int (-4)), from_int (-3); + (from_int (1), from_int (-3)), from_int (-2); + (from_int (1), from_int (-2)), from_int (-1); + (from_int (2), from_int (0)), from_int (2); + (from_int (2), from_int (1)), from_int (3); + (from_int (2), from_int (2)), from_int (4); + (from_int (2), from_int (3)), from_int (5); + (from_int (2), from_int (4)), from_int (6); + (from_int (2), from_int (5)), from_int (7); + (from_int (2), from_int (515)), from_int (517); + (from_int (2), from_int (7)), from_int (9); + (from_int (2), from_int (9)), from_int (11); + (from_int (2), from_int (11)), from_int (13); + (from_int (2), from_int (13)), from_int (15); + (from_int (2), from_int (16)), from_int (18); + (from_int (2), from_int (17)), from_int (19); + (from_int (2), from_int (19)), from_int (21); + (from_int (2), from_int (23)), from_int (25); + (from_int (2), from_int (25)), from_int (27); + (from_int (2), from_int (29)), from_int (31); + (from_int (2), from_int (5026)), from_int (5028); + (from_int (2), from_int (5489)), from_int (5491); + (from_int (2), from_int (-1)), from_int (1); + (from_int (2), from_int (-5)), from_int (-3); + (from_int (2), from_int (-4)), from_int (-2); + (from_int (2), from_int (-3)), from_int (-1); + (from_int (2), from_int (-2)), from_int (0); + (from_int (3), from_int (0)), from_int (3); + (from_int (3), from_int (1)), from_int (4); + (from_int (3), from_int (2)), from_int (5); + (from_int (3), from_int (3)), from_int (6); + (from_int (3), from_int (4)), from_int (7); + (from_int (3), from_int (5)), from_int (8); + (from_int (3), from_int (515)), from_int (518); + (from_int (3), from_int (7)), from_int (10); + (from_int (3), from_int (9)), from_int (12); + (from_int (3), from_int (11)), from_int (14); + (from_int (3), from_int (13)), from_int (16); + (from_int (3), from_int (16)), from_int (19); + (from_int (3), from_int (17)), from_int (20); + (from_int (3), from_int (19)), from_int (22); + (from_int (3), from_int (23)), from_int (26); + (from_int (3), from_int (25)), from_int (28); + (from_int (3), from_int (29)), from_int (32); + (from_int (3), from_int (5026)), from_int (5029); + (from_int (3), from_int (5489)), from_int (5492); + (from_int (3), from_int (-1)), from_int (2); + (from_int (3), from_int (-5)), from_int (-2); + (from_int (3), from_int (-4)), from_int (-1); + (from_int (3), from_int (-3)), from_int (0); + (from_int (3), from_int (-2)), from_int (1); + (from_int (4), from_int (0)), from_int (4); + (from_int (4), from_int (1)), from_int (5); + (from_int (4), from_int (2)), from_int (6); + (from_int (4), from_int (3)), from_int (7); + (from_int (4), from_int (4)), from_int (8); + (from_int (4), from_int (5)), from_int (9); + (from_int (4), from_int (515)), from_int (519); + (from_int (4), from_int (7)), from_int (11); + (from_int (4), from_int (9)), from_int (13); + (from_int (4), from_int (11)), from_int (15); + (from_int (4), from_int (13)), from_int (17); + (from_int (4), from_int (16)), from_int (20); + (from_int (4), from_int (17)), from_int (21); + (from_int (4), from_int (19)), from_int (23); + (from_int (4), from_int (23)), from_int (27); + (from_int (4), from_int (25)), from_int (29); + (from_int (4), from_int (29)), from_int (33); + (from_int (4), from_int (5026)), from_int (5030); + (from_int (4), from_int (5489)), from_int (5493); + (from_int (4), from_int (-1)), from_int (3); + (from_int (4), from_int (-5)), from_int (-1); + (from_int (4), from_int (-4)), from_int (0); + (from_int (4), from_int (-3)), from_int (1); + (from_int (4), from_int (-2)), from_int (2); + (from_int (5), from_int (0)), from_int (5); + (from_int (5), from_int (1)), from_int (6); + (from_int (5), from_int (2)), from_int (7); + (from_int (5), from_int (3)), from_int (8); + (from_int (5), from_int (4)), from_int (9); + (from_int (5), from_int (5)), from_int (10); + (from_int (5), from_int (515)), from_int (520); + (from_int (5), from_int (7)), from_int (12); + (from_int (5), from_int (9)), from_int (14); + (from_int (5), from_int (11)), from_int (16); + (from_int (5), from_int (13)), from_int (18); + (from_int (5), from_int (16)), from_int (21); + (from_int (5), from_int (17)), from_int (22); + (from_int (5), from_int (19)), from_int (24); + (from_int (5), from_int (23)), from_int (28); + (from_int (5), from_int (25)), from_int (30); + (from_int (5), from_int (29)), from_int (34); + (from_int (5), from_int (5026)), from_int (5031); + (from_int (5), from_int (5489)), from_int (5494); + (from_int (5), from_int (-1)), from_int (4); + (from_int (5), from_int (-5)), from_int (0); + (from_int (5), from_int (-4)), from_int (1); + (from_int (5), from_int (-3)), from_int (2); + (from_int (5), from_int (-2)), from_int (3); + (from_int (515), from_int (0)), from_int (515); + (from_int (515), from_int (1)), from_int (516); + (from_int (515), from_int (2)), from_int (517); + (from_int (515), from_int (3)), from_int (518); + (from_int (515), from_int (4)), from_int (519); + (from_int (515), from_int (5)), from_int (520); + (from_int (515), from_int (515)), from_int (1030); + (from_int (515), from_int (7)), from_int (522); + (from_int (515), from_int (9)), from_int (524); + (from_int (515), from_int (11)), from_int (526); + (from_int (515), from_int (13)), from_int (528); + (from_int (515), from_int (16)), from_int (531); + (from_int (515), from_int (17)), from_int (532); + (from_int (515), from_int (19)), from_int (534); + (from_int (515), from_int (23)), from_int (538); + (from_int (515), from_int (25)), from_int (540); + (from_int (515), from_int (29)), from_int (544); + (from_int (515), from_int (5026)), from_int (5541); + (from_int (515), from_int (5489)), from_int (6004); + (from_int (515), from_int (-1)), from_int (514); + (from_int (515), from_int (-5)), from_int (510); + (from_int (515), from_int (-4)), from_int (511); + (from_int (515), from_int (-3)), from_int (512); + (from_int (515), from_int (-2)), from_int (513); + (from_int (7), from_int (0)), from_int (7); + (from_int (7), from_int (1)), from_int (8); + (from_int (7), from_int (2)), from_int (9); + (from_int (7), from_int (3)), from_int (10); + (from_int (7), from_int (4)), from_int (11); + (from_int (7), from_int (5)), from_int (12); + (from_int (7), from_int (515)), from_int (522); + (from_int (7), from_int (7)), from_int (14); + (from_int (7), from_int (9)), from_int (16); + (from_int (7), from_int (11)), from_int (18); + (from_int (7), from_int (13)), from_int (20); + (from_int (7), from_int (16)), from_int (23); + (from_int (7), from_int (17)), from_int (24); + (from_int (7), from_int (19)), from_int (26); + (from_int (7), from_int (23)), from_int (30); + (from_int (7), from_int (25)), from_int (32); + (from_int (7), from_int (29)), from_int (36); + (from_int (7), from_int (5026)), from_int (5033); + (from_int (7), from_int (5489)), from_int (5496); + (from_int (7), from_int (-1)), from_int (6); + (from_int (7), from_int (-5)), from_int (2); + (from_int (7), from_int (-4)), from_int (3); + (from_int (7), from_int (-3)), from_int (4); + (from_int (7), from_int (-2)), from_int (5); + (from_int (9), from_int (0)), from_int (9); + (from_int (9), from_int (1)), from_int (10); + (from_int (9), from_int (2)), from_int (11); + (from_int (9), from_int (3)), from_int (12); + (from_int (9), from_int (4)), from_int (13); + (from_int (9), from_int (5)), from_int (14); + (from_int (9), from_int (515)), from_int (524); + (from_int (9), from_int (7)), from_int (16); + (from_int (9), from_int (9)), from_int (18); + (from_int (9), from_int (11)), from_int (20); + (from_int (9), from_int (13)), from_int (22); + (from_int (9), from_int (16)), from_int (25); + (from_int (9), from_int (17)), from_int (26); + (from_int (9), from_int (19)), from_int (28); + (from_int (9), from_int (23)), from_int (32); + (from_int (9), from_int (25)), from_int (34); + (from_int (9), from_int (29)), from_int (38); + (from_int (9), from_int (5026)), from_int (5035); + (from_int (9), from_int (5489)), from_int (5498); + (from_int (9), from_int (-1)), from_int (8); + (from_int (9), from_int (-5)), from_int (4); + (from_int (9), from_int (-4)), from_int (5); + (from_int (9), from_int (-3)), from_int (6); + (from_int (9), from_int (-2)), from_int (7); + (from_int (11), from_int (0)), from_int (11); + (from_int (11), from_int (1)), from_int (12); + (from_int (11), from_int (2)), from_int (13); + (from_int (11), from_int (3)), from_int (14); + (from_int (11), from_int (4)), from_int (15); + (from_int (11), from_int (5)), from_int (16); + (from_int (11), from_int (515)), from_int (526); + (from_int (11), from_int (7)), from_int (18); + (from_int (11), from_int (9)), from_int (20); + (from_int (11), from_int (11)), from_int (22); + (from_int (11), from_int (13)), from_int (24); + (from_int (11), from_int (16)), from_int (27); + (from_int (11), from_int (17)), from_int (28); + (from_int (11), from_int (19)), from_int (30); + (from_int (11), from_int (23)), from_int (34); + (from_int (11), from_int (25)), from_int (36); + (from_int (11), from_int (29)), from_int (40); + (from_int (11), from_int (5026)), from_int (5037); + (from_int (11), from_int (5489)), from_int (5500); + (from_int (11), from_int (-1)), from_int (10); + (from_int (11), from_int (-5)), from_int (6); + (from_int (11), from_int (-4)), from_int (7); + (from_int (11), from_int (-3)), from_int (8); + (from_int (11), from_int (-2)), from_int (9); + (from_int (13), from_int (0)), from_int (13); + (from_int (13), from_int (1)), from_int (14); + (from_int (13), from_int (2)), from_int (15); + (from_int (13), from_int (3)), from_int (16); + (from_int (13), from_int (4)), from_int (17); + (from_int (13), from_int (5)), from_int (18); + (from_int (13), from_int (515)), from_int (528); + (from_int (13), from_int (7)), from_int (20); + (from_int (13), from_int (9)), from_int (22); + (from_int (13), from_int (11)), from_int (24); + (from_int (13), from_int (13)), from_int (26); + (from_int (13), from_int (16)), from_int (29); + (from_int (13), from_int (17)), from_int (30); + (from_int (13), from_int (19)), from_int (32); + (from_int (13), from_int (23)), from_int (36); + (from_int (13), from_int (25)), from_int (38); + (from_int (13), from_int (29)), from_int (42); + (from_int (13), from_int (5026)), from_int (5039); + (from_int (13), from_int (5489)), from_int (5502); + (from_int (13), from_int (-1)), from_int (12); + (from_int (13), from_int (-5)), from_int (8); + (from_int (13), from_int (-4)), from_int (9); + (from_int (13), from_int (-3)), from_int (10); + (from_int (13), from_int (-2)), from_int (11); + (from_int (16), from_int (0)), from_int (16); + (from_int (16), from_int (1)), from_int (17); + (from_int (16), from_int (2)), from_int (18); + (from_int (16), from_int (3)), from_int (19); + (from_int (16), from_int (4)), from_int (20); + (from_int (16), from_int (5)), from_int (21); + (from_int (16), from_int (515)), from_int (531); + (from_int (16), from_int (7)), from_int (23); + (from_int (16), from_int (9)), from_int (25); + (from_int (16), from_int (11)), from_int (27); + (from_int (16), from_int (13)), from_int (29); + (from_int (16), from_int (16)), from_int (32); + (from_int (16), from_int (17)), from_int (33); + (from_int (16), from_int (19)), from_int (35); + (from_int (16), from_int (23)), from_int (39); + (from_int (16), from_int (25)), from_int (41); + (from_int (16), from_int (29)), from_int (45); + (from_int (16), from_int (5026)), from_int (5042); + (from_int (16), from_int (5489)), from_int (5505); + (from_int (16), from_int (-1)), from_int (15); + (from_int (16), from_int (-5)), from_int (11); + (from_int (16), from_int (-4)), from_int (12); + (from_int (16), from_int (-3)), from_int (13); + (from_int (16), from_int (-2)), from_int (14); + (from_int (17), from_int (0)), from_int (17); + (from_int (17), from_int (1)), from_int (18); + (from_int (17), from_int (2)), from_int (19); + (from_int (17), from_int (3)), from_int (20); + (from_int (17), from_int (4)), from_int (21); + (from_int (17), from_int (5)), from_int (22); + (from_int (17), from_int (515)), from_int (532); + (from_int (17), from_int (7)), from_int (24); + (from_int (17), from_int (9)), from_int (26); + (from_int (17), from_int (11)), from_int (28); + (from_int (17), from_int (13)), from_int (30); + (from_int (17), from_int (16)), from_int (33); + (from_int (17), from_int (17)), from_int (34); + (from_int (17), from_int (19)), from_int (36); + (from_int (17), from_int (23)), from_int (40); + (from_int (17), from_int (25)), from_int (42); + (from_int (17), from_int (29)), from_int (46); + (from_int (17), from_int (5026)), from_int (5043); + (from_int (17), from_int (5489)), from_int (5506); + (from_int (17), from_int (-1)), from_int (16); + (from_int (17), from_int (-5)), from_int (12); + (from_int (17), from_int (-4)), from_int (13); + (from_int (17), from_int (-3)), from_int (14); + (from_int (17), from_int (-2)), from_int (15); + (from_int (19), from_int (0)), from_int (19); + (from_int (19), from_int (1)), from_int (20); + (from_int (19), from_int (2)), from_int (21); + (from_int (19), from_int (3)), from_int (22); + (from_int (19), from_int (4)), from_int (23); + (from_int (19), from_int (5)), from_int (24); + (from_int (19), from_int (515)), from_int (534); + (from_int (19), from_int (7)), from_int (26); + (from_int (19), from_int (9)), from_int (28); + (from_int (19), from_int (11)), from_int (30); + (from_int (19), from_int (13)), from_int (32); + (from_int (19), from_int (16)), from_int (35); + (from_int (19), from_int (17)), from_int (36); + (from_int (19), from_int (19)), from_int (38); + (from_int (19), from_int (23)), from_int (42); + (from_int (19), from_int (25)), from_int (44); + (from_int (19), from_int (29)), from_int (48); + (from_int (19), from_int (5026)), from_int (5045); + (from_int (19), from_int (5489)), from_int (5508); + (from_int (19), from_int (-1)), from_int (18); + (from_int (19), from_int (-5)), from_int (14); + (from_int (19), from_int (-4)), from_int (15); + (from_int (19), from_int (-3)), from_int (16); + (from_int (19), from_int (-2)), from_int (17); + (from_int (23), from_int (0)), from_int (23); + (from_int (23), from_int (1)), from_int (24); + (from_int (23), from_int (2)), from_int (25); + (from_int (23), from_int (3)), from_int (26); + (from_int (23), from_int (4)), from_int (27); + (from_int (23), from_int (5)), from_int (28); + (from_int (23), from_int (515)), from_int (538); + (from_int (23), from_int (7)), from_int (30); + (from_int (23), from_int (9)), from_int (32); + (from_int (23), from_int (11)), from_int (34); + (from_int (23), from_int (13)), from_int (36); + (from_int (23), from_int (16)), from_int (39); + (from_int (23), from_int (17)), from_int (40); + (from_int (23), from_int (19)), from_int (42); + (from_int (23), from_int (23)), from_int (46); + (from_int (23), from_int (25)), from_int (48); + (from_int (23), from_int (29)), from_int (52); + (from_int (23), from_int (5026)), from_int (5049); + (from_int (23), from_int (5489)), from_int (5512); + (from_int (23), from_int (-1)), from_int (22); + (from_int (23), from_int (-5)), from_int (18); + (from_int (23), from_int (-4)), from_int (19); + (from_int (23), from_int (-3)), from_int (20); + (from_int (23), from_int (-2)), from_int (21); + (from_int (25), from_int (0)), from_int (25); + (from_int (25), from_int (1)), from_int (26); + (from_int (25), from_int (2)), from_int (27); + (from_int (25), from_int (3)), from_int (28); + (from_int (25), from_int (4)), from_int (29); + (from_int (25), from_int (5)), from_int (30); + (from_int (25), from_int (515)), from_int (540); + (from_int (25), from_int (7)), from_int (32); + (from_int (25), from_int (9)), from_int (34); + (from_int (25), from_int (11)), from_int (36); + (from_int (25), from_int (13)), from_int (38); + (from_int (25), from_int (16)), from_int (41); + (from_int (25), from_int (17)), from_int (42); + (from_int (25), from_int (19)), from_int (44); + (from_int (25), from_int (23)), from_int (48); + (from_int (25), from_int (25)), from_int (50); + (from_int (25), from_int (29)), from_int (54); + (from_int (25), from_int (5026)), from_int (5051); + (from_int (25), from_int (5489)), from_int (5514); + (from_int (25), from_int (-1)), from_int (24); + (from_int (25), from_int (-5)), from_int (20); + (from_int (25), from_int (-4)), from_int (21); + (from_int (25), from_int (-3)), from_int (22); + (from_int (25), from_int (-2)), from_int (23); + (from_int (29), from_int (0)), from_int (29); + (from_int (29), from_int (1)), from_int (30); + (from_int (29), from_int (2)), from_int (31); + (from_int (29), from_int (3)), from_int (32); + (from_int (29), from_int (4)), from_int (33); + (from_int (29), from_int (5)), from_int (34); + (from_int (29), from_int (515)), from_int (544); + (from_int (29), from_int (7)), from_int (36); + (from_int (29), from_int (9)), from_int (38); + (from_int (29), from_int (11)), from_int (40); + (from_int (29), from_int (13)), from_int (42); + (from_int (29), from_int (16)), from_int (45); + (from_int (29), from_int (17)), from_int (46); + (from_int (29), from_int (19)), from_int (48); + (from_int (29), from_int (23)), from_int (52); + (from_int (29), from_int (25)), from_int (54); + (from_int (29), from_int (29)), from_int (58); + (from_int (29), from_int (5026)), from_int (5055); + (from_int (29), from_int (5489)), from_int (5518); + (from_int (29), from_int (-1)), from_int (28); + (from_int (29), from_int (-5)), from_int (24); + (from_int (29), from_int (-4)), from_int (25); + (from_int (29), from_int (-3)), from_int (26); + (from_int (29), from_int (-2)), from_int (27); + (from_int (5026), from_int (0)), from_int (5026); + (from_int (5026), from_int (1)), from_int (5027); + (from_int (5026), from_int (2)), from_int (5028); + (from_int (5026), from_int (3)), from_int (5029); + (from_int (5026), from_int (4)), from_int (5030); + (from_int (5026), from_int (5)), from_int (5031); + (from_int (5026), from_int (515)), from_int (5541); + (from_int (5026), from_int (7)), from_int (5033); + (from_int (5026), from_int (9)), from_int (5035); + (from_int (5026), from_int (11)), from_int (5037); + (from_int (5026), from_int (13)), from_int (5039); + (from_int (5026), from_int (16)), from_int (5042); + (from_int (5026), from_int (17)), from_int (5043); + (from_int (5026), from_int (19)), from_int (5045); + (from_int (5026), from_int (23)), from_int (5049); + (from_int (5026), from_int (25)), from_int (5051); + (from_int (5026), from_int (29)), from_int (5055); + (from_int (5026), from_int (5026)), from_int (10052); + (from_int (5026), from_int (5489)), from_int (10515); + (from_int (5026), from_int (-1)), from_int (5025); + (from_int (5026), from_int (-5)), from_int (5021); + (from_int (5026), from_int (-4)), from_int (5022); + (from_int (5026), from_int (-3)), from_int (5023); + (from_int (5026), from_int (-2)), from_int (5024); + (from_int (5489), from_int (0)), from_int (5489); + (from_int (5489), from_int (1)), from_int (5490); + (from_int (5489), from_int (2)), from_int (5491); + (from_int (5489), from_int (3)), from_int (5492); + (from_int (5489), from_int (4)), from_int (5493); + (from_int (5489), from_int (5)), from_int (5494); + (from_int (5489), from_int (515)), from_int (6004); + (from_int (5489), from_int (7)), from_int (5496); + (from_int (5489), from_int (9)), from_int (5498); + (from_int (5489), from_int (11)), from_int (5500); + (from_int (5489), from_int (13)), from_int (5502); + (from_int (5489), from_int (16)), from_int (5505); + (from_int (5489), from_int (17)), from_int (5506); + (from_int (5489), from_int (19)), from_int (5508); + (from_int (5489), from_int (23)), from_int (5512); + (from_int (5489), from_int (25)), from_int (5514); + (from_int (5489), from_int (29)), from_int (5518); + (from_int (5489), from_int (5026)), from_int (10515); + (from_int (5489), from_int (5489)), from_int (10978); + (from_int (5489), from_int (-1)), from_int (5488); + (from_int (5489), from_int (-5)), from_int (5484); + (from_int (5489), from_int (-4)), from_int (5485); + (from_int (5489), from_int (-3)), from_int (5486); + (from_int (5489), from_int (-2)), from_int (5487); + (from_int (-1), from_int (0)), from_int (-1); + (from_int (-1), from_int (1)), from_int (0); + (from_int (-1), from_int (2)), from_int (1); + (from_int (-1), from_int (3)), from_int (2); + (from_int (-1), from_int (4)), from_int (3); + (from_int (-1), from_int (5)), from_int (4); + (from_int (-1), from_int (515)), from_int (514); + (from_int (-1), from_int (7)), from_int (6); + (from_int (-1), from_int (9)), from_int (8); + (from_int (-1), from_int (11)), from_int (10); + (from_int (-1), from_int (13)), from_int (12); + (from_int (-1), from_int (16)), from_int (15); + (from_int (-1), from_int (17)), from_int (16); + (from_int (-1), from_int (19)), from_int (18); + (from_int (-1), from_int (23)), from_int (22); + (from_int (-1), from_int (25)), from_int (24); + (from_int (-1), from_int (29)), from_int (28); + (from_int (-1), from_int (5026)), from_int (5025); + (from_int (-1), from_int (5489)), from_int (5488); + (from_int (-1), from_int (-1)), from_int (-2); + (from_int (-1), from_int (-5)), from_int (-6); + (from_int (-1), from_int (-4)), from_int (-5); + (from_int (-1), from_int (-3)), from_int (-4); + (from_int (-1), from_int (-2)), from_int (-3); + (from_int (-5), from_int (0)), from_int (-5); + (from_int (-5), from_int (1)), from_int (-4); + (from_int (-5), from_int (2)), from_int (-3); + (from_int (-5), from_int (3)), from_int (-2); + (from_int (-5), from_int (4)), from_int (-1); + (from_int (-5), from_int (5)), from_int (0); + (from_int (-5), from_int (515)), from_int (510); + (from_int (-5), from_int (7)), from_int (2); + (from_int (-5), from_int (9)), from_int (4); + (from_int (-5), from_int (11)), from_int (6); + (from_int (-5), from_int (13)), from_int (8); + (from_int (-5), from_int (16)), from_int (11); + (from_int (-5), from_int (17)), from_int (12); + (from_int (-5), from_int (19)), from_int (14); + (from_int (-5), from_int (23)), from_int (18); + (from_int (-5), from_int (25)), from_int (20); + (from_int (-5), from_int (29)), from_int (24); + (from_int (-5), from_int (5026)), from_int (5021); + (from_int (-5), from_int (5489)), from_int (5484); + (from_int (-5), from_int (-1)), from_int (-6); + (from_int (-5), from_int (-5)), from_int (-10); + (from_int (-5), from_int (-4)), from_int (-9); + (from_int (-5), from_int (-3)), from_int (-8); + (from_int (-5), from_int (-2)), from_int (-7); + (from_int (-4), from_int (0)), from_int (-4); + (from_int (-4), from_int (1)), from_int (-3); + (from_int (-4), from_int (2)), from_int (-2); + (from_int (-4), from_int (3)), from_int (-1); + (from_int (-4), from_int (4)), from_int (0); + (from_int (-4), from_int (5)), from_int (1); + (from_int (-4), from_int (515)), from_int (511); + (from_int (-4), from_int (7)), from_int (3); + (from_int (-4), from_int (9)), from_int (5); + (from_int (-4), from_int (11)), from_int (7); + (from_int (-4), from_int (13)), from_int (9); + (from_int (-4), from_int (16)), from_int (12); + (from_int (-4), from_int (17)), from_int (13); + (from_int (-4), from_int (19)), from_int (15); + (from_int (-4), from_int (23)), from_int (19); + (from_int (-4), from_int (25)), from_int (21); + (from_int (-4), from_int (29)), from_int (25); + (from_int (-4), from_int (5026)), from_int (5022); + (from_int (-4), from_int (5489)), from_int (5485); + (from_int (-4), from_int (-1)), from_int (-5); + (from_int (-4), from_int (-5)), from_int (-9); + (from_int (-4), from_int (-4)), from_int (-8); + (from_int (-4), from_int (-3)), from_int (-7); + (from_int (-4), from_int (-2)), from_int (-6); + (from_int (-3), from_int (0)), from_int (-3); + (from_int (-3), from_int (1)), from_int (-2); + (from_int (-3), from_int (2)), from_int (-1); + (from_int (-3), from_int (3)), from_int (0); + (from_int (-3), from_int (4)), from_int (1); + (from_int (-3), from_int (5)), from_int (2); + (from_int (-3), from_int (515)), from_int (512); + (from_int (-3), from_int (7)), from_int (4); + (from_int (-3), from_int (9)), from_int (6); + (from_int (-3), from_int (11)), from_int (8); + (from_int (-3), from_int (13)), from_int (10); + (from_int (-3), from_int (16)), from_int (13); + (from_int (-3), from_int (17)), from_int (14); + (from_int (-3), from_int (19)), from_int (16); + (from_int (-3), from_int (23)), from_int (20); + (from_int (-3), from_int (25)), from_int (22); + (from_int (-3), from_int (29)), from_int (26); + (from_int (-3), from_int (5026)), from_int (5023); + (from_int (-3), from_int (5489)), from_int (5486); + (from_int (-3), from_int (-1)), from_int (-4); + (from_int (-3), from_int (-5)), from_int (-8); + (from_int (-3), from_int (-4)), from_int (-7); + (from_int (-3), from_int (-3)), from_int (-6); + (from_int (-3), from_int (-2)), from_int (-5); + (from_int (-2), from_int (0)), from_int (-2); + (from_int (-2), from_int (1)), from_int (-1); + (from_int (-2), from_int (2)), from_int (0); + (from_int (-2), from_int (3)), from_int (1); + (from_int (-2), from_int (4)), from_int (2); + (from_int (-2), from_int (5)), from_int (3); + (from_int (-2), from_int (515)), from_int (513); + (from_int (-2), from_int (7)), from_int (5); + (from_int (-2), from_int (9)), from_int (7); + (from_int (-2), from_int (11)), from_int (9); + (from_int (-2), from_int (13)), from_int (11); + (from_int (-2), from_int (16)), from_int (14); + (from_int (-2), from_int (17)), from_int (15); + (from_int (-2), from_int (19)), from_int (17); + (from_int (-2), from_int (23)), from_int (21); + (from_int (-2), from_int (25)), from_int (23); + (from_int (-2), from_int (29)), from_int (27); + (from_int (-2), from_int (5026)), from_int (5024); + (from_int (-2), from_int (5489)), from_int (5487); + (from_int (-2), from_int (-1)), from_int (-3); + (from_int (-2), from_int (-5)), from_int (-7); + (from_int (-2), from_int (-4)), from_int (-6); + (from_int (-2), from_int (-3)), from_int (-5); + (from_int (-2), from_int (-2)), from_int (-4); + ] + in + run_test template_2_1 "add_b" add_b t_list +;; + +let () = + let t_list = + [ + (from_int (0), from_int (0)), from_int (0); + (from_int (0), from_int (1)), from_int (-1); + (from_int (0), from_int (2)), from_int (-2); + (from_int (0), from_int (3)), from_int (-3); + (from_int (0), from_int (4)), from_int (-4); + (from_int (0), from_int (5)), from_int (-5); + (from_int (0), from_int (515)), from_int (-515); + (from_int (0), from_int (7)), from_int (-7); + (from_int (0), from_int (9)), from_int (-9); + (from_int (0), from_int (11)), from_int (-11); + (from_int (0), from_int (13)), from_int (-13); + (from_int (0), from_int (16)), from_int (-16); + (from_int (0), from_int (17)), from_int (-17); + (from_int (0), from_int (19)), from_int (-19); + (from_int (0), from_int (23)), from_int (-23); + (from_int (0), from_int (25)), from_int (-25); + (from_int (0), from_int (29)), from_int (-29); + (from_int (0), from_int (5026)), from_int (-5026); + (from_int (0), from_int (5489)), from_int (-5489); + (from_int (0), from_int (-1)), from_int (1); + (from_int (0), from_int (-5)), from_int (5); + (from_int (0), from_int (-4)), from_int (4); + (from_int (0), from_int (-3)), from_int (3); + (from_int (0), from_int (-2)), from_int (2); + (from_int (1), from_int (0)), from_int (1); + (from_int (1), from_int (1)), from_int (0); + (from_int (1), from_int (2)), from_int (-1); + (from_int (1), from_int (3)), from_int (-2); + (from_int (1), from_int (4)), from_int (-3); + (from_int (1), from_int (5)), from_int (-4); + (from_int (1), from_int (515)), from_int (-514); + (from_int (1), from_int (7)), from_int (-6); + (from_int (1), from_int (9)), from_int (-8); + (from_int (1), from_int (11)), from_int (-10); + (from_int (1), from_int (13)), from_int (-12); + (from_int (1), from_int (16)), from_int (-15); + (from_int (1), from_int (17)), from_int (-16); + (from_int (1), from_int (19)), from_int (-18); + (from_int (1), from_int (23)), from_int (-22); + (from_int (1), from_int (25)), from_int (-24); + (from_int (1), from_int (29)), from_int (-28); + (from_int (1), from_int (5026)), from_int (-5025); + (from_int (1), from_int (5489)), from_int (-5488); + (from_int (1), from_int (-1)), from_int (2); + (from_int (1), from_int (-5)), from_int (6); + (from_int (1), from_int (-4)), from_int (5); + (from_int (1), from_int (-3)), from_int (4); + (from_int (1), from_int (-2)), from_int (3); + (from_int (2), from_int (0)), from_int (2); + (from_int (2), from_int (1)), from_int (1); + (from_int (2), from_int (2)), from_int (0); + (from_int (2), from_int (3)), from_int (-1); + (from_int (2), from_int (4)), from_int (-2); + (from_int (2), from_int (5)), from_int (-3); + (from_int (2), from_int (515)), from_int (-513); + (from_int (2), from_int (7)), from_int (-5); + (from_int (2), from_int (9)), from_int (-7); + (from_int (2), from_int (11)), from_int (-9); + (from_int (2), from_int (13)), from_int (-11); + (from_int (2), from_int (16)), from_int (-14); + (from_int (2), from_int (17)), from_int (-15); + (from_int (2), from_int (19)), from_int (-17); + (from_int (2), from_int (23)), from_int (-21); + (from_int (2), from_int (25)), from_int (-23); + (from_int (2), from_int (29)), from_int (-27); + (from_int (2), from_int (5026)), from_int (-5024); + (from_int (2), from_int (5489)), from_int (-5487); + (from_int (2), from_int (-1)), from_int (3); + (from_int (2), from_int (-5)), from_int (7); + (from_int (2), from_int (-4)), from_int (6); + (from_int (2), from_int (-3)), from_int (5); + (from_int (2), from_int (-2)), from_int (4); + (from_int (3), from_int (0)), from_int (3); + (from_int (3), from_int (1)), from_int (2); + (from_int (3), from_int (2)), from_int (1); + (from_int (3), from_int (3)), from_int (0); + (from_int (3), from_int (4)), from_int (-1); + (from_int (3), from_int (5)), from_int (-2); + (from_int (3), from_int (515)), from_int (-512); + (from_int (3), from_int (7)), from_int (-4); + (from_int (3), from_int (9)), from_int (-6); + (from_int (3), from_int (11)), from_int (-8); + (from_int (3), from_int (13)), from_int (-10); + (from_int (3), from_int (16)), from_int (-13); + (from_int (3), from_int (17)), from_int (-14); + (from_int (3), from_int (19)), from_int (-16); + (from_int (3), from_int (23)), from_int (-20); + (from_int (3), from_int (25)), from_int (-22); + (from_int (3), from_int (29)), from_int (-26); + (from_int (3), from_int (5026)), from_int (-5023); + (from_int (3), from_int (5489)), from_int (-5486); + (from_int (3), from_int (-1)), from_int (4); + (from_int (3), from_int (-5)), from_int (8); + (from_int (3), from_int (-4)), from_int (7); + (from_int (3), from_int (-3)), from_int (6); + (from_int (3), from_int (-2)), from_int (5); + (from_int (4), from_int (0)), from_int (4); + (from_int (4), from_int (1)), from_int (3); + (from_int (4), from_int (2)), from_int (2); + (from_int (4), from_int (3)), from_int (1); + (from_int (4), from_int (4)), from_int (0); + (from_int (4), from_int (5)), from_int (-1); + (from_int (4), from_int (515)), from_int (-511); + (from_int (4), from_int (7)), from_int (-3); + (from_int (4), from_int (9)), from_int (-5); + (from_int (4), from_int (11)), from_int (-7); + (from_int (4), from_int (13)), from_int (-9); + (from_int (4), from_int (16)), from_int (-12); + (from_int (4), from_int (17)), from_int (-13); + (from_int (4), from_int (19)), from_int (-15); + (from_int (4), from_int (23)), from_int (-19); + (from_int (4), from_int (25)), from_int (-21); + (from_int (4), from_int (29)), from_int (-25); + (from_int (4), from_int (5026)), from_int (-5022); + (from_int (4), from_int (5489)), from_int (-5485); + (from_int (4), from_int (-1)), from_int (5); + (from_int (4), from_int (-5)), from_int (9); + (from_int (4), from_int (-4)), from_int (8); + (from_int (4), from_int (-3)), from_int (7); + (from_int (4), from_int (-2)), from_int (6); + (from_int (5), from_int (0)), from_int (5); + (from_int (5), from_int (1)), from_int (4); + (from_int (5), from_int (2)), from_int (3); + (from_int (5), from_int (3)), from_int (2); + (from_int (5), from_int (4)), from_int (1); + (from_int (5), from_int (5)), from_int (0); + (from_int (5), from_int (515)), from_int (-510); + (from_int (5), from_int (7)), from_int (-2); + (from_int (5), from_int (9)), from_int (-4); + (from_int (5), from_int (11)), from_int (-6); + (from_int (5), from_int (13)), from_int (-8); + (from_int (5), from_int (16)), from_int (-11); + (from_int (5), from_int (17)), from_int (-12); + (from_int (5), from_int (19)), from_int (-14); + (from_int (5), from_int (23)), from_int (-18); + (from_int (5), from_int (25)), from_int (-20); + (from_int (5), from_int (29)), from_int (-24); + (from_int (5), from_int (5026)), from_int (-5021); + (from_int (5), from_int (5489)), from_int (-5484); + (from_int (5), from_int (-1)), from_int (6); + (from_int (5), from_int (-5)), from_int (10); + (from_int (5), from_int (-4)), from_int (9); + (from_int (5), from_int (-3)), from_int (8); + (from_int (5), from_int (-2)), from_int (7); + (from_int (515), from_int (0)), from_int (515); + (from_int (515), from_int (1)), from_int (514); + (from_int (515), from_int (2)), from_int (513); + (from_int (515), from_int (3)), from_int (512); + (from_int (515), from_int (4)), from_int (511); + (from_int (515), from_int (5)), from_int (510); + (from_int (515), from_int (515)), from_int (0); + (from_int (515), from_int (7)), from_int (508); + (from_int (515), from_int (9)), from_int (506); + (from_int (515), from_int (11)), from_int (504); + (from_int (515), from_int (13)), from_int (502); + (from_int (515), from_int (16)), from_int (499); + (from_int (515), from_int (17)), from_int (498); + (from_int (515), from_int (19)), from_int (496); + (from_int (515), from_int (23)), from_int (492); + (from_int (515), from_int (25)), from_int (490); + (from_int (515), from_int (29)), from_int (486); + (from_int (515), from_int (5026)), from_int (-4511); + (from_int (515), from_int (5489)), from_int (-4974); + (from_int (515), from_int (-1)), from_int (516); + (from_int (515), from_int (-5)), from_int (520); + (from_int (515), from_int (-4)), from_int (519); + (from_int (515), from_int (-3)), from_int (518); + (from_int (515), from_int (-2)), from_int (517); + (from_int (7), from_int (0)), from_int (7); + (from_int (7), from_int (1)), from_int (6); + (from_int (7), from_int (2)), from_int (5); + (from_int (7), from_int (3)), from_int (4); + (from_int (7), from_int (4)), from_int (3); + (from_int (7), from_int (5)), from_int (2); + (from_int (7), from_int (515)), from_int (-508); + (from_int (7), from_int (7)), from_int (0); + (from_int (7), from_int (9)), from_int (-2); + (from_int (7), from_int (11)), from_int (-4); + (from_int (7), from_int (13)), from_int (-6); + (from_int (7), from_int (16)), from_int (-9); + (from_int (7), from_int (17)), from_int (-10); + (from_int (7), from_int (19)), from_int (-12); + (from_int (7), from_int (23)), from_int (-16); + (from_int (7), from_int (25)), from_int (-18); + (from_int (7), from_int (29)), from_int (-22); + (from_int (7), from_int (5026)), from_int (-5019); + (from_int (7), from_int (5489)), from_int (-5482); + (from_int (7), from_int (-1)), from_int (8); + (from_int (7), from_int (-5)), from_int (12); + (from_int (7), from_int (-4)), from_int (11); + (from_int (7), from_int (-3)), from_int (10); + (from_int (7), from_int (-2)), from_int (9); + (from_int (9), from_int (0)), from_int (9); + (from_int (9), from_int (1)), from_int (8); + (from_int (9), from_int (2)), from_int (7); + (from_int (9), from_int (3)), from_int (6); + (from_int (9), from_int (4)), from_int (5); + (from_int (9), from_int (5)), from_int (4); + (from_int (9), from_int (515)), from_int (-506); + (from_int (9), from_int (7)), from_int (2); + (from_int (9), from_int (9)), from_int (0); + (from_int (9), from_int (11)), from_int (-2); + (from_int (9), from_int (13)), from_int (-4); + (from_int (9), from_int (16)), from_int (-7); + (from_int (9), from_int (17)), from_int (-8); + (from_int (9), from_int (19)), from_int (-10); + (from_int (9), from_int (23)), from_int (-14); + (from_int (9), from_int (25)), from_int (-16); + (from_int (9), from_int (29)), from_int (-20); + (from_int (9), from_int (5026)), from_int (-5017); + (from_int (9), from_int (5489)), from_int (-5480); + (from_int (9), from_int (-1)), from_int (10); + (from_int (9), from_int (-5)), from_int (14); + (from_int (9), from_int (-4)), from_int (13); + (from_int (9), from_int (-3)), from_int (12); + (from_int (9), from_int (-2)), from_int (11); + (from_int (11), from_int (0)), from_int (11); + (from_int (11), from_int (1)), from_int (10); + (from_int (11), from_int (2)), from_int (9); + (from_int (11), from_int (3)), from_int (8); + (from_int (11), from_int (4)), from_int (7); + (from_int (11), from_int (5)), from_int (6); + (from_int (11), from_int (515)), from_int (-504); + (from_int (11), from_int (7)), from_int (4); + (from_int (11), from_int (9)), from_int (2); + (from_int (11), from_int (11)), from_int (0); + (from_int (11), from_int (13)), from_int (-2); + (from_int (11), from_int (16)), from_int (-5); + (from_int (11), from_int (17)), from_int (-6); + (from_int (11), from_int (19)), from_int (-8); + (from_int (11), from_int (23)), from_int (-12); + (from_int (11), from_int (25)), from_int (-14); + (from_int (11), from_int (29)), from_int (-18); + (from_int (11), from_int (5026)), from_int (-5015); + (from_int (11), from_int (5489)), from_int (-5478); + (from_int (11), from_int (-1)), from_int (12); + (from_int (11), from_int (-5)), from_int (16); + (from_int (11), from_int (-4)), from_int (15); + (from_int (11), from_int (-3)), from_int (14); + (from_int (11), from_int (-2)), from_int (13); + (from_int (13), from_int (0)), from_int (13); + (from_int (13), from_int (1)), from_int (12); + (from_int (13), from_int (2)), from_int (11); + (from_int (13), from_int (3)), from_int (10); + (from_int (13), from_int (4)), from_int (9); + (from_int (13), from_int (5)), from_int (8); + (from_int (13), from_int (515)), from_int (-502); + (from_int (13), from_int (7)), from_int (6); + (from_int (13), from_int (9)), from_int (4); + (from_int (13), from_int (11)), from_int (2); + (from_int (13), from_int (13)), from_int (0); + (from_int (13), from_int (16)), from_int (-3); + (from_int (13), from_int (17)), from_int (-4); + (from_int (13), from_int (19)), from_int (-6); + (from_int (13), from_int (23)), from_int (-10); + (from_int (13), from_int (25)), from_int (-12); + (from_int (13), from_int (29)), from_int (-16); + (from_int (13), from_int (5026)), from_int (-5013); + (from_int (13), from_int (5489)), from_int (-5476); + (from_int (13), from_int (-1)), from_int (14); + (from_int (13), from_int (-5)), from_int (18); + (from_int (13), from_int (-4)), from_int (17); + (from_int (13), from_int (-3)), from_int (16); + (from_int (13), from_int (-2)), from_int (15); + (from_int (16), from_int (0)), from_int (16); + (from_int (16), from_int (1)), from_int (15); + (from_int (16), from_int (2)), from_int (14); + (from_int (16), from_int (3)), from_int (13); + (from_int (16), from_int (4)), from_int (12); + (from_int (16), from_int (5)), from_int (11); + (from_int (16), from_int (515)), from_int (-499); + (from_int (16), from_int (7)), from_int (9); + (from_int (16), from_int (9)), from_int (7); + (from_int (16), from_int (11)), from_int (5); + (from_int (16), from_int (13)), from_int (3); + (from_int (16), from_int (16)), from_int (0); + (from_int (16), from_int (17)), from_int (-1); + (from_int (16), from_int (19)), from_int (-3); + (from_int (16), from_int (23)), from_int (-7); + (from_int (16), from_int (25)), from_int (-9); + (from_int (16), from_int (29)), from_int (-13); + (from_int (16), from_int (5026)), from_int (-5010); + (from_int (16), from_int (5489)), from_int (-5473); + (from_int (16), from_int (-1)), from_int (17); + (from_int (16), from_int (-5)), from_int (21); + (from_int (16), from_int (-4)), from_int (20); + (from_int (16), from_int (-3)), from_int (19); + (from_int (16), from_int (-2)), from_int (18); + (from_int (17), from_int (0)), from_int (17); + (from_int (17), from_int (1)), from_int (16); + (from_int (17), from_int (2)), from_int (15); + (from_int (17), from_int (3)), from_int (14); + (from_int (17), from_int (4)), from_int (13); + (from_int (17), from_int (5)), from_int (12); + (from_int (17), from_int (515)), from_int (-498); + (from_int (17), from_int (7)), from_int (10); + (from_int (17), from_int (9)), from_int (8); + (from_int (17), from_int (11)), from_int (6); + (from_int (17), from_int (13)), from_int (4); + (from_int (17), from_int (16)), from_int (1); + (from_int (17), from_int (17)), from_int (0); + (from_int (17), from_int (19)), from_int (-2); + (from_int (17), from_int (23)), from_int (-6); + (from_int (17), from_int (25)), from_int (-8); + (from_int (17), from_int (29)), from_int (-12); + (from_int (17), from_int (5026)), from_int (-5009); + (from_int (17), from_int (5489)), from_int (-5472); + (from_int (17), from_int (-1)), from_int (18); + (from_int (17), from_int (-5)), from_int (22); + (from_int (17), from_int (-4)), from_int (21); + (from_int (17), from_int (-3)), from_int (20); + (from_int (17), from_int (-2)), from_int (19); + (from_int (19), from_int (0)), from_int (19); + (from_int (19), from_int (1)), from_int (18); + (from_int (19), from_int (2)), from_int (17); + (from_int (19), from_int (3)), from_int (16); + (from_int (19), from_int (4)), from_int (15); + (from_int (19), from_int (5)), from_int (14); + (from_int (19), from_int (515)), from_int (-496); + (from_int (19), from_int (7)), from_int (12); + (from_int (19), from_int (9)), from_int (10); + (from_int (19), from_int (11)), from_int (8); + (from_int (19), from_int (13)), from_int (6); + (from_int (19), from_int (16)), from_int (3); + (from_int (19), from_int (17)), from_int (2); + (from_int (19), from_int (19)), from_int (0); + (from_int (19), from_int (23)), from_int (-4); + (from_int (19), from_int (25)), from_int (-6); + (from_int (19), from_int (29)), from_int (-10); + (from_int (19), from_int (5026)), from_int (-5007); + (from_int (19), from_int (5489)), from_int (-5470); + (from_int (19), from_int (-1)), from_int (20); + (from_int (19), from_int (-5)), from_int (24); + (from_int (19), from_int (-4)), from_int (23); + (from_int (19), from_int (-3)), from_int (22); + (from_int (19), from_int (-2)), from_int (21); + (from_int (23), from_int (0)), from_int (23); + (from_int (23), from_int (1)), from_int (22); + (from_int (23), from_int (2)), from_int (21); + (from_int (23), from_int (3)), from_int (20); + (from_int (23), from_int (4)), from_int (19); + (from_int (23), from_int (5)), from_int (18); + (from_int (23), from_int (515)), from_int (-492); + (from_int (23), from_int (7)), from_int (16); + (from_int (23), from_int (9)), from_int (14); + (from_int (23), from_int (11)), from_int (12); + (from_int (23), from_int (13)), from_int (10); + (from_int (23), from_int (16)), from_int (7); + (from_int (23), from_int (17)), from_int (6); + (from_int (23), from_int (19)), from_int (4); + (from_int (23), from_int (23)), from_int (0); + (from_int (23), from_int (25)), from_int (-2); + (from_int (23), from_int (29)), from_int (-6); + (from_int (23), from_int (5026)), from_int (-5003); + (from_int (23), from_int (5489)), from_int (-5466); + (from_int (23), from_int (-1)), from_int (24); + (from_int (23), from_int (-5)), from_int (28); + (from_int (23), from_int (-4)), from_int (27); + (from_int (23), from_int (-3)), from_int (26); + (from_int (23), from_int (-2)), from_int (25); + (from_int (25), from_int (0)), from_int (25); + (from_int (25), from_int (1)), from_int (24); + (from_int (25), from_int (2)), from_int (23); + (from_int (25), from_int (3)), from_int (22); + (from_int (25), from_int (4)), from_int (21); + (from_int (25), from_int (5)), from_int (20); + (from_int (25), from_int (515)), from_int (-490); + (from_int (25), from_int (7)), from_int (18); + (from_int (25), from_int (9)), from_int (16); + (from_int (25), from_int (11)), from_int (14); + (from_int (25), from_int (13)), from_int (12); + (from_int (25), from_int (16)), from_int (9); + (from_int (25), from_int (17)), from_int (8); + (from_int (25), from_int (19)), from_int (6); + (from_int (25), from_int (23)), from_int (2); + (from_int (25), from_int (25)), from_int (0); + (from_int (25), from_int (29)), from_int (-4); + (from_int (25), from_int (5026)), from_int (-5001); + (from_int (25), from_int (5489)), from_int (-5464); + (from_int (25), from_int (-1)), from_int (26); + (from_int (25), from_int (-5)), from_int (30); + (from_int (25), from_int (-4)), from_int (29); + (from_int (25), from_int (-3)), from_int (28); + (from_int (25), from_int (-2)), from_int (27); + (from_int (29), from_int (0)), from_int (29); + (from_int (29), from_int (1)), from_int (28); + (from_int (29), from_int (2)), from_int (27); + (from_int (29), from_int (3)), from_int (26); + (from_int (29), from_int (4)), from_int (25); + (from_int (29), from_int (5)), from_int (24); + (from_int (29), from_int (515)), from_int (-486); + (from_int (29), from_int (7)), from_int (22); + (from_int (29), from_int (9)), from_int (20); + (from_int (29), from_int (11)), from_int (18); + (from_int (29), from_int (13)), from_int (16); + (from_int (29), from_int (16)), from_int (13); + (from_int (29), from_int (17)), from_int (12); + (from_int (29), from_int (19)), from_int (10); + (from_int (29), from_int (23)), from_int (6); + (from_int (29), from_int (25)), from_int (4); + (from_int (29), from_int (29)), from_int (0); + (from_int (29), from_int (5026)), from_int (-4997); + (from_int (29), from_int (5489)), from_int (-5460); + (from_int (29), from_int (-1)), from_int (30); + (from_int (29), from_int (-5)), from_int (34); + (from_int (29), from_int (-4)), from_int (33); + (from_int (29), from_int (-3)), from_int (32); + (from_int (29), from_int (-2)), from_int (31); + (from_int (5026), from_int (0)), from_int (5026); + (from_int (5026), from_int (1)), from_int (5025); + (from_int (5026), from_int (2)), from_int (5024); + (from_int (5026), from_int (3)), from_int (5023); + (from_int (5026), from_int (4)), from_int (5022); + (from_int (5026), from_int (5)), from_int (5021); + (from_int (5026), from_int (515)), from_int (4511); + (from_int (5026), from_int (7)), from_int (5019); + (from_int (5026), from_int (9)), from_int (5017); + (from_int (5026), from_int (11)), from_int (5015); + (from_int (5026), from_int (13)), from_int (5013); + (from_int (5026), from_int (16)), from_int (5010); + (from_int (5026), from_int (17)), from_int (5009); + (from_int (5026), from_int (19)), from_int (5007); + (from_int (5026), from_int (23)), from_int (5003); + (from_int (5026), from_int (25)), from_int (5001); + (from_int (5026), from_int (29)), from_int (4997); + (from_int (5026), from_int (5026)), from_int (0); + (from_int (5026), from_int (5489)), from_int (-463); + (from_int (5026), from_int (-1)), from_int (5027); + (from_int (5026), from_int (-5)), from_int (5031); + (from_int (5026), from_int (-4)), from_int (5030); + (from_int (5026), from_int (-3)), from_int (5029); + (from_int (5026), from_int (-2)), from_int (5028); + (from_int (5489), from_int (0)), from_int (5489); + (from_int (5489), from_int (1)), from_int (5488); + (from_int (5489), from_int (2)), from_int (5487); + (from_int (5489), from_int (3)), from_int (5486); + (from_int (5489), from_int (4)), from_int (5485); + (from_int (5489), from_int (5)), from_int (5484); + (from_int (5489), from_int (515)), from_int (4974); + (from_int (5489), from_int (7)), from_int (5482); + (from_int (5489), from_int (9)), from_int (5480); + (from_int (5489), from_int (11)), from_int (5478); + (from_int (5489), from_int (13)), from_int (5476); + (from_int (5489), from_int (16)), from_int (5473); + (from_int (5489), from_int (17)), from_int (5472); + (from_int (5489), from_int (19)), from_int (5470); + (from_int (5489), from_int (23)), from_int (5466); + (from_int (5489), from_int (25)), from_int (5464); + (from_int (5489), from_int (29)), from_int (5460); + (from_int (5489), from_int (5026)), from_int (463); + (from_int (5489), from_int (5489)), from_int (0); + (from_int (5489), from_int (-1)), from_int (5490); + (from_int (5489), from_int (-5)), from_int (5494); + (from_int (5489), from_int (-4)), from_int (5493); + (from_int (5489), from_int (-3)), from_int (5492); + (from_int (5489), from_int (-2)), from_int (5491); + (from_int (-1), from_int (0)), from_int (-1); + (from_int (-1), from_int (1)), from_int (-2); + (from_int (-1), from_int (2)), from_int (-3); + (from_int (-1), from_int (3)), from_int (-4); + (from_int (-1), from_int (4)), from_int (-5); + (from_int (-1), from_int (5)), from_int (-6); + (from_int (-1), from_int (515)), from_int (-516); + (from_int (-1), from_int (7)), from_int (-8); + (from_int (-1), from_int (9)), from_int (-10); + (from_int (-1), from_int (11)), from_int (-12); + (from_int (-1), from_int (13)), from_int (-14); + (from_int (-1), from_int (16)), from_int (-17); + (from_int (-1), from_int (17)), from_int (-18); + (from_int (-1), from_int (19)), from_int (-20); + (from_int (-1), from_int (23)), from_int (-24); + (from_int (-1), from_int (25)), from_int (-26); + (from_int (-1), from_int (29)), from_int (-30); + (from_int (-1), from_int (5026)), from_int (-5027); + (from_int (-1), from_int (5489)), from_int (-5490); + (from_int (-1), from_int (-1)), from_int (0); + (from_int (-1), from_int (-5)), from_int (4); + (from_int (-1), from_int (-4)), from_int (3); + (from_int (-1), from_int (-3)), from_int (2); + (from_int (-1), from_int (-2)), from_int (1); + (from_int (-5), from_int (0)), from_int (-5); + (from_int (-5), from_int (1)), from_int (-6); + (from_int (-5), from_int (2)), from_int (-7); + (from_int (-5), from_int (3)), from_int (-8); + (from_int (-5), from_int (4)), from_int (-9); + (from_int (-5), from_int (5)), from_int (-10); + (from_int (-5), from_int (515)), from_int (-520); + (from_int (-5), from_int (7)), from_int (-12); + (from_int (-5), from_int (9)), from_int (-14); + (from_int (-5), from_int (11)), from_int (-16); + (from_int (-5), from_int (13)), from_int (-18); + (from_int (-5), from_int (16)), from_int (-21); + (from_int (-5), from_int (17)), from_int (-22); + (from_int (-5), from_int (19)), from_int (-24); + (from_int (-5), from_int (23)), from_int (-28); + (from_int (-5), from_int (25)), from_int (-30); + (from_int (-5), from_int (29)), from_int (-34); + (from_int (-5), from_int (5026)), from_int (-5031); + (from_int (-5), from_int (5489)), from_int (-5494); + (from_int (-5), from_int (-1)), from_int (-4); + (from_int (-5), from_int (-5)), from_int (0); + (from_int (-5), from_int (-4)), from_int (-1); + (from_int (-5), from_int (-3)), from_int (-2); + (from_int (-5), from_int (-2)), from_int (-3); + (from_int (-4), from_int (0)), from_int (-4); + (from_int (-4), from_int (1)), from_int (-5); + (from_int (-4), from_int (2)), from_int (-6); + (from_int (-4), from_int (3)), from_int (-7); + (from_int (-4), from_int (4)), from_int (-8); + (from_int (-4), from_int (5)), from_int (-9); + (from_int (-4), from_int (515)), from_int (-519); + (from_int (-4), from_int (7)), from_int (-11); + (from_int (-4), from_int (9)), from_int (-13); + (from_int (-4), from_int (11)), from_int (-15); + (from_int (-4), from_int (13)), from_int (-17); + (from_int (-4), from_int (16)), from_int (-20); + (from_int (-4), from_int (17)), from_int (-21); + (from_int (-4), from_int (19)), from_int (-23); + (from_int (-4), from_int (23)), from_int (-27); + (from_int (-4), from_int (25)), from_int (-29); + (from_int (-4), from_int (29)), from_int (-33); + (from_int (-4), from_int (5026)), from_int (-5030); + (from_int (-4), from_int (5489)), from_int (-5493); + (from_int (-4), from_int (-1)), from_int (-3); + (from_int (-4), from_int (-5)), from_int (1); + (from_int (-4), from_int (-4)), from_int (0); + (from_int (-4), from_int (-3)), from_int (-1); + (from_int (-4), from_int (-2)), from_int (-2); + (from_int (-3), from_int (0)), from_int (-3); + (from_int (-3), from_int (1)), from_int (-4); + (from_int (-3), from_int (2)), from_int (-5); + (from_int (-3), from_int (3)), from_int (-6); + (from_int (-3), from_int (4)), from_int (-7); + (from_int (-3), from_int (5)), from_int (-8); + (from_int (-3), from_int (515)), from_int (-518); + (from_int (-3), from_int (7)), from_int (-10); + (from_int (-3), from_int (9)), from_int (-12); + (from_int (-3), from_int (11)), from_int (-14); + (from_int (-3), from_int (13)), from_int (-16); + (from_int (-3), from_int (16)), from_int (-19); + (from_int (-3), from_int (17)), from_int (-20); + (from_int (-3), from_int (19)), from_int (-22); + (from_int (-3), from_int (23)), from_int (-26); + (from_int (-3), from_int (25)), from_int (-28); + (from_int (-3), from_int (29)), from_int (-32); + (from_int (-3), from_int (5026)), from_int (-5029); + (from_int (-3), from_int (5489)), from_int (-5492); + (from_int (-3), from_int (-1)), from_int (-2); + (from_int (-3), from_int (-5)), from_int (2); + (from_int (-3), from_int (-4)), from_int (1); + (from_int (-3), from_int (-3)), from_int (0); + (from_int (-3), from_int (-2)), from_int (-1); + (from_int (-2), from_int (0)), from_int (-2); + (from_int (-2), from_int (1)), from_int (-3); + (from_int (-2), from_int (2)), from_int (-4); + (from_int (-2), from_int (3)), from_int (-5); + (from_int (-2), from_int (4)), from_int (-6); + (from_int (-2), from_int (5)), from_int (-7); + (from_int (-2), from_int (515)), from_int (-517); + (from_int (-2), from_int (7)), from_int (-9); + (from_int (-2), from_int (9)), from_int (-11); + (from_int (-2), from_int (11)), from_int (-13); + (from_int (-2), from_int (13)), from_int (-15); + (from_int (-2), from_int (16)), from_int (-18); + (from_int (-2), from_int (17)), from_int (-19); + (from_int (-2), from_int (19)), from_int (-21); + (from_int (-2), from_int (23)), from_int (-25); + (from_int (-2), from_int (25)), from_int (-27); + (from_int (-2), from_int (29)), from_int (-31); + (from_int (-2), from_int (5026)), from_int (-5028); + (from_int (-2), from_int (5489)), from_int (-5491); + (from_int (-2), from_int (-1)), from_int (-1); + (from_int (-2), from_int (-5)), from_int (3); + (from_int (-2), from_int (-4)), from_int (2); + (from_int (-2), from_int (-3)), from_int (1); + (from_int (-2), from_int (-2)), from_int (0); + ] + in + run_test template_2_1 "diff_b" diff_b t_list +;; + +let () = + let t_list = + [ + (from_int (0), 0), from_int (0); + (from_int (0), 1), from_int (0); + (from_int (0), 2), from_int (0); + (from_int (0), 3), from_int (0); + (from_int (0), 4), from_int (0); + (from_int (0), 5), from_int (0); + (from_int (1), 0), from_int (1); + (from_int (1), 1), from_int (2); + (from_int (1), 2), from_int (4); + (from_int (1), 3), from_int (8); + (from_int (1), 4), from_int (16); + (from_int (1), 5), from_int (32); + (from_int (2), 0), from_int (2); + (from_int (2), 1), from_int (4); + (from_int (2), 2), from_int (8); + (from_int (2), 3), from_int (16); + (from_int (2), 4), from_int (32); + (from_int (2), 5), from_int (64); + (from_int (3), 0), from_int (3); + (from_int (3), 1), from_int (6); + (from_int (3), 2), from_int (12); + (from_int (3), 3), from_int (24); + (from_int (3), 4), from_int (48); + (from_int (3), 5), from_int (96); + (from_int (4), 0), from_int (4); + (from_int (4), 1), from_int (8); + (from_int (4), 2), from_int (16); + (from_int (4), 3), from_int (32); + (from_int (4), 4), from_int (64); + (from_int (4), 5), from_int (128); + (from_int (5), 0), from_int (5); + (from_int (5), 1), from_int (10); + (from_int (5), 2), from_int (20); + (from_int (5), 3), from_int (40); + (from_int (5), 4), from_int (80); + (from_int (5), 5), from_int (160); + (from_int (-2), 0), from_int (-2); + (from_int (-2), 1), from_int (-4); + (from_int (-2), 2), from_int (-8); + (from_int (-2), 3), from_int (-16); + (from_int (-2), 4), from_int (-32); + (from_int (-2), 5), from_int (-64); + (from_int (-5), 0), from_int (-5); + (from_int (-5), 1), from_int (-10); + (from_int (-5), 2), from_int (-20); + (from_int (-5), 3), from_int (-40); + (from_int (-5), 4), from_int (-80); + (from_int (-5), 5), from_int (-160); + (from_int (-4), 0), from_int (-4); + (from_int (-4), 1), from_int (-8); + (from_int (-4), 2), from_int (-16); + (from_int (-4), 3), from_int (-32); + (from_int (-4), 4), from_int (-64); + (from_int (-4), 5), from_int (-128); + (from_int (-3), 0), from_int (-3); + (from_int (-3), 1), from_int (-6); + (from_int (-3), 2), from_int (-12); + (from_int (-3), 3), from_int (-24); + (from_int (-3), 4), from_int (-48); + (from_int (-3), 5), from_int (-96); + (from_int (-1), 0), from_int (-1); + (from_int (-1), 1), from_int (-2); + (from_int (-1), 2), from_int (-4); + (from_int (-1), 3), from_int (-8); + (from_int (-1), 4), from_int (-16); + (from_int (-1), 5), from_int (-32); + ] + in + run_test template_11i_1 "shift" shift t_list +;; + +let () = + let t_list = + [ + (from_int (0), from_int (0)), from_int (0); + (from_int (0), from_int (1)), from_int (0); + (from_int (0), from_int (2)), from_int (0); + (from_int (0), from_int (3)), from_int (0); + (from_int (0), from_int (4)), from_int (0); + (from_int (0), from_int (5)), from_int (0); + (from_int (0), from_int (515)), from_int (0); + (from_int (0), from_int (7)), from_int (0); + (from_int (0), from_int (9)), from_int (0); + (from_int (0), from_int (11)), from_int (0); + (from_int (0), from_int (13)), from_int (0); + (from_int (0), from_int (16)), from_int (0); + (from_int (0), from_int (17)), from_int (0); + (from_int (0), from_int (19)), from_int (0); + (from_int (0), from_int (23)), from_int (0); + (from_int (0), from_int (25)), from_int (0); + (from_int (0), from_int (29)), from_int (0); + (from_int (0), from_int (5026)), from_int (0); + (from_int (0), from_int (5489)), from_int (0); + (from_int (0), from_int (-1)), from_int (0); + (from_int (0), from_int (-5)), from_int (0); + (from_int (0), from_int (-4)), from_int (0); + (from_int (0), from_int (-3)), from_int (0); + (from_int (0), from_int (-2)), from_int (0); + (from_int (1), from_int (0)), from_int (0); + (from_int (1), from_int (1)), from_int (1); + (from_int (1), from_int (2)), from_int (2); + (from_int (1), from_int (3)), from_int (3); + (from_int (1), from_int (4)), from_int (4); + (from_int (1), from_int (5)), from_int (5); + (from_int (1), from_int (515)), from_int (515); + (from_int (1), from_int (7)), from_int (7); + (from_int (1), from_int (9)), from_int (9); + (from_int (1), from_int (11)), from_int (11); + (from_int (1), from_int (13)), from_int (13); + (from_int (1), from_int (16)), from_int (16); + (from_int (1), from_int (17)), from_int (17); + (from_int (1), from_int (19)), from_int (19); + (from_int (1), from_int (23)), from_int (23); + (from_int (1), from_int (25)), from_int (25); + (from_int (1), from_int (29)), from_int (29); + (from_int (1), from_int (5026)), from_int (5026); + (from_int (1), from_int (5489)), from_int (5489); + (from_int (1), from_int (-1)), from_int (-1); + (from_int (1), from_int (-5)), from_int (-5); + (from_int (1), from_int (-4)), from_int (-4); + (from_int (1), from_int (-3)), from_int (-3); + (from_int (1), from_int (-2)), from_int (-2); + (from_int (2), from_int (0)), from_int (0); + (from_int (2), from_int (1)), from_int (2); + (from_int (2), from_int (2)), from_int (4); + (from_int (2), from_int (3)), from_int (6); + (from_int (2), from_int (4)), from_int (8); + (from_int (2), from_int (5)), from_int (10); + (from_int (2), from_int (515)), from_int (1030); + (from_int (2), from_int (7)), from_int (14); + (from_int (2), from_int (9)), from_int (18); + (from_int (2), from_int (11)), from_int (22); + (from_int (2), from_int (13)), from_int (26); + (from_int (2), from_int (16)), from_int (32); + (from_int (2), from_int (17)), from_int (34); + (from_int (2), from_int (19)), from_int (38); + (from_int (2), from_int (23)), from_int (46); + (from_int (2), from_int (25)), from_int (50); + (from_int (2), from_int (29)), from_int (58); + (from_int (2), from_int (5026)), from_int (10052); + (from_int (2), from_int (5489)), from_int (10978); + (from_int (2), from_int (-1)), from_int (-2); + (from_int (2), from_int (-5)), from_int (-10); + (from_int (2), from_int (-4)), from_int (-8); + (from_int (2), from_int (-3)), from_int (-6); + (from_int (2), from_int (-2)), from_int (-4); + (from_int (3), from_int (0)), from_int (0); + (from_int (3), from_int (1)), from_int (3); + (from_int (3), from_int (2)), from_int (6); + (from_int (3), from_int (3)), from_int (9); + (from_int (3), from_int (4)), from_int (12); + (from_int (3), from_int (5)), from_int (15); + (from_int (3), from_int (515)), from_int (1545); + (from_int (3), from_int (7)), from_int (21); + (from_int (3), from_int (9)), from_int (27); + (from_int (3), from_int (11)), from_int (33); + (from_int (3), from_int (13)), from_int (39); + (from_int (3), from_int (16)), from_int (48); + (from_int (3), from_int (17)), from_int (51); + (from_int (3), from_int (19)), from_int (57); + (from_int (3), from_int (23)), from_int (69); + (from_int (3), from_int (25)), from_int (75); + (from_int (3), from_int (29)), from_int (87); + (from_int (3), from_int (5026)), from_int (15078); + (from_int (3), from_int (5489)), from_int (16467); + (from_int (3), from_int (-1)), from_int (-3); + (from_int (3), from_int (-5)), from_int (-15); + (from_int (3), from_int (-4)), from_int (-12); + (from_int (3), from_int (-3)), from_int (-9); + (from_int (3), from_int (-2)), from_int (-6); + (from_int (4), from_int (0)), from_int (0); + (from_int (4), from_int (1)), from_int (4); + (from_int (4), from_int (2)), from_int (8); + (from_int (4), from_int (3)), from_int (12); + (from_int (4), from_int (4)), from_int (16); + (from_int (4), from_int (5)), from_int (20); + (from_int (4), from_int (515)), from_int (2060); + (from_int (4), from_int (7)), from_int (28); + (from_int (4), from_int (9)), from_int (36); + (from_int (4), from_int (11)), from_int (44); + (from_int (4), from_int (13)), from_int (52); + (from_int (4), from_int (16)), from_int (64); + (from_int (4), from_int (17)), from_int (68); + (from_int (4), from_int (19)), from_int (76); + (from_int (4), from_int (23)), from_int (92); + (from_int (4), from_int (25)), from_int (100); + (from_int (4), from_int (29)), from_int (116); + (from_int (4), from_int (5026)), from_int (20104); + (from_int (4), from_int (5489)), from_int (21956); + (from_int (4), from_int (-1)), from_int (-4); + (from_int (4), from_int (-5)), from_int (-20); + (from_int (4), from_int (-4)), from_int (-16); + (from_int (4), from_int (-3)), from_int (-12); + (from_int (4), from_int (-2)), from_int (-8); + (from_int (5), from_int (0)), from_int (0); + (from_int (5), from_int (1)), from_int (5); + (from_int (5), from_int (2)), from_int (10); + (from_int (5), from_int (3)), from_int (15); + (from_int (5), from_int (4)), from_int (20); + (from_int (5), from_int (5)), from_int (25); + (from_int (5), from_int (515)), from_int (2575); + (from_int (5), from_int (7)), from_int (35); + (from_int (5), from_int (9)), from_int (45); + (from_int (5), from_int (11)), from_int (55); + (from_int (5), from_int (13)), from_int (65); + (from_int (5), from_int (16)), from_int (80); + (from_int (5), from_int (17)), from_int (85); + (from_int (5), from_int (19)), from_int (95); + (from_int (5), from_int (23)), from_int (115); + (from_int (5), from_int (25)), from_int (125); + (from_int (5), from_int (29)), from_int (145); + (from_int (5), from_int (5026)), from_int (25130); + (from_int (5), from_int (5489)), from_int (27445); + (from_int (5), from_int (-1)), from_int (-5); + (from_int (5), from_int (-5)), from_int (-25); + (from_int (5), from_int (-4)), from_int (-20); + (from_int (5), from_int (-3)), from_int (-15); + (from_int (5), from_int (-2)), from_int (-10); + (from_int (515), from_int (0)), from_int (0); + (from_int (515), from_int (1)), from_int (515); + (from_int (515), from_int (2)), from_int (1030); + (from_int (515), from_int (3)), from_int (1545); + (from_int (515), from_int (4)), from_int (2060); + (from_int (515), from_int (5)), from_int (2575); + (from_int (515), from_int (515)), from_int (265225); + (from_int (515), from_int (7)), from_int (3605); + (from_int (515), from_int (9)), from_int (4635); + (from_int (515), from_int (11)), from_int (5665); + (from_int (515), from_int (13)), from_int (6695); + (from_int (515), from_int (16)), from_int (8240); + (from_int (515), from_int (17)), from_int (8755); + (from_int (515), from_int (19)), from_int (9785); + (from_int (515), from_int (23)), from_int (11845); + (from_int (515), from_int (25)), from_int (12875); + (from_int (515), from_int (29)), from_int (14935); + (from_int (515), from_int (5026)), from_int (2588390); + (from_int (515), from_int (5489)), from_int (2826835); + (from_int (515), from_int (-1)), from_int (-515); + (from_int (515), from_int (-5)), from_int (-2575); + (from_int (515), from_int (-4)), from_int (-2060); + (from_int (515), from_int (-3)), from_int (-1545); + (from_int (515), from_int (-2)), from_int (-1030); + (from_int (7), from_int (0)), from_int (0); + (from_int (7), from_int (1)), from_int (7); + (from_int (7), from_int (2)), from_int (14); + (from_int (7), from_int (3)), from_int (21); + (from_int (7), from_int (4)), from_int (28); + (from_int (7), from_int (5)), from_int (35); + (from_int (7), from_int (515)), from_int (3605); + (from_int (7), from_int (7)), from_int (49); + (from_int (7), from_int (9)), from_int (63); + (from_int (7), from_int (11)), from_int (77); + (from_int (7), from_int (13)), from_int (91); + (from_int (7), from_int (16)), from_int (112); + (from_int (7), from_int (17)), from_int (119); + (from_int (7), from_int (19)), from_int (133); + (from_int (7), from_int (23)), from_int (161); + (from_int (7), from_int (25)), from_int (175); + (from_int (7), from_int (29)), from_int (203); + (from_int (7), from_int (5026)), from_int (35182); + (from_int (7), from_int (5489)), from_int (38423); + (from_int (7), from_int (-1)), from_int (-7); + (from_int (7), from_int (-5)), from_int (-35); + (from_int (7), from_int (-4)), from_int (-28); + (from_int (7), from_int (-3)), from_int (-21); + (from_int (7), from_int (-2)), from_int (-14); + (from_int (9), from_int (0)), from_int (0); + (from_int (9), from_int (1)), from_int (9); + (from_int (9), from_int (2)), from_int (18); + (from_int (9), from_int (3)), from_int (27); + (from_int (9), from_int (4)), from_int (36); + (from_int (9), from_int (5)), from_int (45); + (from_int (9), from_int (515)), from_int (4635); + (from_int (9), from_int (7)), from_int (63); + (from_int (9), from_int (9)), from_int (81); + (from_int (9), from_int (11)), from_int (99); + (from_int (9), from_int (13)), from_int (117); + (from_int (9), from_int (16)), from_int (144); + (from_int (9), from_int (17)), from_int (153); + (from_int (9), from_int (19)), from_int (171); + (from_int (9), from_int (23)), from_int (207); + (from_int (9), from_int (25)), from_int (225); + (from_int (9), from_int (29)), from_int (261); + (from_int (9), from_int (5026)), from_int (45234); + (from_int (9), from_int (5489)), from_int (49401); + (from_int (9), from_int (-1)), from_int (-9); + (from_int (9), from_int (-5)), from_int (-45); + (from_int (9), from_int (-4)), from_int (-36); + (from_int (9), from_int (-3)), from_int (-27); + (from_int (9), from_int (-2)), from_int (-18); + (from_int (11), from_int (0)), from_int (0); + (from_int (11), from_int (1)), from_int (11); + (from_int (11), from_int (2)), from_int (22); + (from_int (11), from_int (3)), from_int (33); + (from_int (11), from_int (4)), from_int (44); + (from_int (11), from_int (5)), from_int (55); + (from_int (11), from_int (515)), from_int (5665); + (from_int (11), from_int (7)), from_int (77); + (from_int (11), from_int (9)), from_int (99); + (from_int (11), from_int (11)), from_int (121); + (from_int (11), from_int (13)), from_int (143); + (from_int (11), from_int (16)), from_int (176); + (from_int (11), from_int (17)), from_int (187); + (from_int (11), from_int (19)), from_int (209); + (from_int (11), from_int (23)), from_int (253); + (from_int (11), from_int (25)), from_int (275); + (from_int (11), from_int (29)), from_int (319); + (from_int (11), from_int (5026)), from_int (55286); + (from_int (11), from_int (5489)), from_int (60379); + (from_int (11), from_int (-1)), from_int (-11); + (from_int (11), from_int (-5)), from_int (-55); + (from_int (11), from_int (-4)), from_int (-44); + (from_int (11), from_int (-3)), from_int (-33); + (from_int (11), from_int (-2)), from_int (-22); + (from_int (13), from_int (0)), from_int (0); + (from_int (13), from_int (1)), from_int (13); + (from_int (13), from_int (2)), from_int (26); + (from_int (13), from_int (3)), from_int (39); + (from_int (13), from_int (4)), from_int (52); + (from_int (13), from_int (5)), from_int (65); + (from_int (13), from_int (515)), from_int (6695); + (from_int (13), from_int (7)), from_int (91); + (from_int (13), from_int (9)), from_int (117); + (from_int (13), from_int (11)), from_int (143); + (from_int (13), from_int (13)), from_int (169); + (from_int (13), from_int (16)), from_int (208); + (from_int (13), from_int (17)), from_int (221); + (from_int (13), from_int (19)), from_int (247); + (from_int (13), from_int (23)), from_int (299); + (from_int (13), from_int (25)), from_int (325); + (from_int (13), from_int (29)), from_int (377); + (from_int (13), from_int (5026)), from_int (65338); + (from_int (13), from_int (5489)), from_int (71357); + (from_int (13), from_int (-1)), from_int (-13); + (from_int (13), from_int (-5)), from_int (-65); + (from_int (13), from_int (-4)), from_int (-52); + (from_int (13), from_int (-3)), from_int (-39); + (from_int (13), from_int (-2)), from_int (-26); + (from_int (16), from_int (0)), from_int (0); + (from_int (16), from_int (1)), from_int (16); + (from_int (16), from_int (2)), from_int (32); + (from_int (16), from_int (3)), from_int (48); + (from_int (16), from_int (4)), from_int (64); + (from_int (16), from_int (5)), from_int (80); + (from_int (16), from_int (515)), from_int (8240); + (from_int (16), from_int (7)), from_int (112); + (from_int (16), from_int (9)), from_int (144); + (from_int (16), from_int (11)), from_int (176); + (from_int (16), from_int (13)), from_int (208); + (from_int (16), from_int (16)), from_int (256); + (from_int (16), from_int (17)), from_int (272); + (from_int (16), from_int (19)), from_int (304); + (from_int (16), from_int (23)), from_int (368); + (from_int (16), from_int (25)), from_int (400); + (from_int (16), from_int (29)), from_int (464); + (from_int (16), from_int (5026)), from_int (80416); + (from_int (16), from_int (5489)), from_int (87824); + (from_int (16), from_int (-1)), from_int (-16); + (from_int (16), from_int (-5)), from_int (-80); + (from_int (16), from_int (-4)), from_int (-64); + (from_int (16), from_int (-3)), from_int (-48); + (from_int (16), from_int (-2)), from_int (-32); + (from_int (17), from_int (0)), from_int (0); + (from_int (17), from_int (1)), from_int (17); + (from_int (17), from_int (2)), from_int (34); + (from_int (17), from_int (3)), from_int (51); + (from_int (17), from_int (4)), from_int (68); + (from_int (17), from_int (5)), from_int (85); + (from_int (17), from_int (515)), from_int (8755); + (from_int (17), from_int (7)), from_int (119); + (from_int (17), from_int (9)), from_int (153); + (from_int (17), from_int (11)), from_int (187); + (from_int (17), from_int (13)), from_int (221); + (from_int (17), from_int (16)), from_int (272); + (from_int (17), from_int (17)), from_int (289); + (from_int (17), from_int (19)), from_int (323); + (from_int (17), from_int (23)), from_int (391); + (from_int (17), from_int (25)), from_int (425); + (from_int (17), from_int (29)), from_int (493); + (from_int (17), from_int (5026)), from_int (85442); + (from_int (17), from_int (5489)), from_int (93313); + (from_int (17), from_int (-1)), from_int (-17); + (from_int (17), from_int (-5)), from_int (-85); + (from_int (17), from_int (-4)), from_int (-68); + (from_int (17), from_int (-3)), from_int (-51); + (from_int (17), from_int (-2)), from_int (-34); + (from_int (19), from_int (0)), from_int (0); + (from_int (19), from_int (1)), from_int (19); + (from_int (19), from_int (2)), from_int (38); + (from_int (19), from_int (3)), from_int (57); + (from_int (19), from_int (4)), from_int (76); + (from_int (19), from_int (5)), from_int (95); + (from_int (19), from_int (515)), from_int (9785); + (from_int (19), from_int (7)), from_int (133); + (from_int (19), from_int (9)), from_int (171); + (from_int (19), from_int (11)), from_int (209); + (from_int (19), from_int (13)), from_int (247); + (from_int (19), from_int (16)), from_int (304); + (from_int (19), from_int (17)), from_int (323); + (from_int (19), from_int (19)), from_int (361); + (from_int (19), from_int (23)), from_int (437); + (from_int (19), from_int (25)), from_int (475); + (from_int (19), from_int (29)), from_int (551); + (from_int (19), from_int (5026)), from_int (95494); + (from_int (19), from_int (5489)), from_int (104291); + (from_int (19), from_int (-1)), from_int (-19); + (from_int (19), from_int (-5)), from_int (-95); + (from_int (19), from_int (-4)), from_int (-76); + (from_int (19), from_int (-3)), from_int (-57); + (from_int (19), from_int (-2)), from_int (-38); + (from_int (23), from_int (0)), from_int (0); + (from_int (23), from_int (1)), from_int (23); + (from_int (23), from_int (2)), from_int (46); + (from_int (23), from_int (3)), from_int (69); + (from_int (23), from_int (4)), from_int (92); + (from_int (23), from_int (5)), from_int (115); + (from_int (23), from_int (515)), from_int (11845); + (from_int (23), from_int (7)), from_int (161); + (from_int (23), from_int (9)), from_int (207); + (from_int (23), from_int (11)), from_int (253); + (from_int (23), from_int (13)), from_int (299); + (from_int (23), from_int (16)), from_int (368); + (from_int (23), from_int (17)), from_int (391); + (from_int (23), from_int (19)), from_int (437); + (from_int (23), from_int (23)), from_int (529); + (from_int (23), from_int (25)), from_int (575); + (from_int (23), from_int (29)), from_int (667); + (from_int (23), from_int (5026)), from_int (115598); + (from_int (23), from_int (5489)), from_int (126247); + (from_int (23), from_int (-1)), from_int (-23); + (from_int (23), from_int (-5)), from_int (-115); + (from_int (23), from_int (-4)), from_int (-92); + (from_int (23), from_int (-3)), from_int (-69); + (from_int (23), from_int (-2)), from_int (-46); + (from_int (25), from_int (0)), from_int (0); + (from_int (25), from_int (1)), from_int (25); + (from_int (25), from_int (2)), from_int (50); + (from_int (25), from_int (3)), from_int (75); + (from_int (25), from_int (4)), from_int (100); + (from_int (25), from_int (5)), from_int (125); + (from_int (25), from_int (515)), from_int (12875); + (from_int (25), from_int (7)), from_int (175); + (from_int (25), from_int (9)), from_int (225); + (from_int (25), from_int (11)), from_int (275); + (from_int (25), from_int (13)), from_int (325); + (from_int (25), from_int (16)), from_int (400); + (from_int (25), from_int (17)), from_int (425); + (from_int (25), from_int (19)), from_int (475); + (from_int (25), from_int (23)), from_int (575); + (from_int (25), from_int (25)), from_int (625); + (from_int (25), from_int (29)), from_int (725); + (from_int (25), from_int (5026)), from_int (125650); + (from_int (25), from_int (5489)), from_int (137225); + (from_int (25), from_int (-1)), from_int (-25); + (from_int (25), from_int (-5)), from_int (-125); + (from_int (25), from_int (-4)), from_int (-100); + (from_int (25), from_int (-3)), from_int (-75); + (from_int (25), from_int (-2)), from_int (-50); + (from_int (29), from_int (0)), from_int (0); + (from_int (29), from_int (1)), from_int (29); + (from_int (29), from_int (2)), from_int (58); + (from_int (29), from_int (3)), from_int (87); + (from_int (29), from_int (4)), from_int (116); + (from_int (29), from_int (5)), from_int (145); + (from_int (29), from_int (515)), from_int (14935); + (from_int (29), from_int (7)), from_int (203); + (from_int (29), from_int (9)), from_int (261); + (from_int (29), from_int (11)), from_int (319); + (from_int (29), from_int (13)), from_int (377); + (from_int (29), from_int (16)), from_int (464); + (from_int (29), from_int (17)), from_int (493); + (from_int (29), from_int (19)), from_int (551); + (from_int (29), from_int (23)), from_int (667); + (from_int (29), from_int (25)), from_int (725); + (from_int (29), from_int (29)), from_int (841); + (from_int (29), from_int (5026)), from_int (145754); + (from_int (29), from_int (5489)), from_int (159181); + (from_int (29), from_int (-1)), from_int (-29); + (from_int (29), from_int (-5)), from_int (-145); + (from_int (29), from_int (-4)), from_int (-116); + (from_int (29), from_int (-3)), from_int (-87); + (from_int (29), from_int (-2)), from_int (-58); + (from_int (5026), from_int (0)), from_int (0); + (from_int (5026), from_int (1)), from_int (5026); + (from_int (5026), from_int (2)), from_int (10052); + (from_int (5026), from_int (3)), from_int (15078); + (from_int (5026), from_int (4)), from_int (20104); + (from_int (5026), from_int (5)), from_int (25130); + (from_int (5026), from_int (515)), from_int (2588390); + (from_int (5026), from_int (7)), from_int (35182); + (from_int (5026), from_int (9)), from_int (45234); + (from_int (5026), from_int (11)), from_int (55286); + (from_int (5026), from_int (13)), from_int (65338); + (from_int (5026), from_int (16)), from_int (80416); + (from_int (5026), from_int (17)), from_int (85442); + (from_int (5026), from_int (19)), from_int (95494); + (from_int (5026), from_int (23)), from_int (115598); + (from_int (5026), from_int (25)), from_int (125650); + (from_int (5026), from_int (29)), from_int (145754); + (from_int (5026), from_int (5026)), from_int (25260676); + (from_int (5026), from_int (5489)), from_int (27587714); + (from_int (5026), from_int (-1)), from_int (-5026); + (from_int (5026), from_int (-5)), from_int (-25130); + (from_int (5026), from_int (-4)), from_int (-20104); + (from_int (5026), from_int (-3)), from_int (-15078); + (from_int (5026), from_int (-2)), from_int (-10052); + (from_int (5489), from_int (0)), from_int (0); + (from_int (5489), from_int (1)), from_int (5489); + (from_int (5489), from_int (2)), from_int (10978); + (from_int (5489), from_int (3)), from_int (16467); + (from_int (5489), from_int (4)), from_int (21956); + (from_int (5489), from_int (5)), from_int (27445); + (from_int (5489), from_int (515)), from_int (2826835); + (from_int (5489), from_int (7)), from_int (38423); + (from_int (5489), from_int (9)), from_int (49401); + (from_int (5489), from_int (11)), from_int (60379); + (from_int (5489), from_int (13)), from_int (71357); + (from_int (5489), from_int (16)), from_int (87824); + (from_int (5489), from_int (17)), from_int (93313); + (from_int (5489), from_int (19)), from_int (104291); + (from_int (5489), from_int (23)), from_int (126247); + (from_int (5489), from_int (25)), from_int (137225); + (from_int (5489), from_int (29)), from_int (159181); + (from_int (5489), from_int (5026)), from_int (27587714); + (from_int (5489), from_int (5489)), from_int (30129121); + (from_int (5489), from_int (-1)), from_int (-5489); + (from_int (5489), from_int (-5)), from_int (-27445); + (from_int (5489), from_int (-4)), from_int (-21956); + (from_int (5489), from_int (-3)), from_int (-16467); + (from_int (5489), from_int (-2)), from_int (-10978); + (from_int (-1), from_int (0)), from_int (0); + (from_int (-1), from_int (1)), from_int (-1); + (from_int (-1), from_int (2)), from_int (-2); + (from_int (-1), from_int (3)), from_int (-3); + (from_int (-1), from_int (4)), from_int (-4); + (from_int (-1), from_int (5)), from_int (-5); + (from_int (-1), from_int (515)), from_int (-515); + (from_int (-1), from_int (7)), from_int (-7); + (from_int (-1), from_int (9)), from_int (-9); + (from_int (-1), from_int (11)), from_int (-11); + (from_int (-1), from_int (13)), from_int (-13); + (from_int (-1), from_int (16)), from_int (-16); + (from_int (-1), from_int (17)), from_int (-17); + (from_int (-1), from_int (19)), from_int (-19); + (from_int (-1), from_int (23)), from_int (-23); + (from_int (-1), from_int (25)), from_int (-25); + (from_int (-1), from_int (29)), from_int (-29); + (from_int (-1), from_int (5026)), from_int (-5026); + (from_int (-1), from_int (5489)), from_int (-5489); + (from_int (-1), from_int (-1)), from_int (1); + (from_int (-1), from_int (-5)), from_int (5); + (from_int (-1), from_int (-4)), from_int (4); + (from_int (-1), from_int (-3)), from_int (3); + (from_int (-1), from_int (-2)), from_int (2); + (from_int (-5), from_int (0)), from_int (0); + (from_int (-5), from_int (1)), from_int (-5); + (from_int (-5), from_int (2)), from_int (-10); + (from_int (-5), from_int (3)), from_int (-15); + (from_int (-5), from_int (4)), from_int (-20); + (from_int (-5), from_int (5)), from_int (-25); + (from_int (-5), from_int (515)), from_int (-2575); + (from_int (-5), from_int (7)), from_int (-35); + (from_int (-5), from_int (9)), from_int (-45); + (from_int (-5), from_int (11)), from_int (-55); + (from_int (-5), from_int (13)), from_int (-65); + (from_int (-5), from_int (16)), from_int (-80); + (from_int (-5), from_int (17)), from_int (-85); + (from_int (-5), from_int (19)), from_int (-95); + (from_int (-5), from_int (23)), from_int (-115); + (from_int (-5), from_int (25)), from_int (-125); + (from_int (-5), from_int (29)), from_int (-145); + (from_int (-5), from_int (5026)), from_int (-25130); + (from_int (-5), from_int (5489)), from_int (-27445); + (from_int (-5), from_int (-1)), from_int (5); + (from_int (-5), from_int (-5)), from_int (25); + (from_int (-5), from_int (-4)), from_int (20); + (from_int (-5), from_int (-3)), from_int (15); + (from_int (-5), from_int (-2)), from_int (10); + (from_int (-4), from_int (0)), from_int (0); + (from_int (-4), from_int (1)), from_int (-4); + (from_int (-4), from_int (2)), from_int (-8); + (from_int (-4), from_int (3)), from_int (-12); + (from_int (-4), from_int (4)), from_int (-16); + (from_int (-4), from_int (5)), from_int (-20); + (from_int (-4), from_int (515)), from_int (-2060); + (from_int (-4), from_int (7)), from_int (-28); + (from_int (-4), from_int (9)), from_int (-36); + (from_int (-4), from_int (11)), from_int (-44); + (from_int (-4), from_int (13)), from_int (-52); + (from_int (-4), from_int (16)), from_int (-64); + (from_int (-4), from_int (17)), from_int (-68); + (from_int (-4), from_int (19)), from_int (-76); + (from_int (-4), from_int (23)), from_int (-92); + (from_int (-4), from_int (25)), from_int (-100); + (from_int (-4), from_int (29)), from_int (-116); + (from_int (-4), from_int (5026)), from_int (-20104); + (from_int (-4), from_int (5489)), from_int (-21956); + (from_int (-4), from_int (-1)), from_int (4); + (from_int (-4), from_int (-5)), from_int (20); + (from_int (-4), from_int (-4)), from_int (16); + (from_int (-4), from_int (-3)), from_int (12); + (from_int (-4), from_int (-2)), from_int (8); + (from_int (-3), from_int (0)), from_int (0); + (from_int (-3), from_int (1)), from_int (-3); + (from_int (-3), from_int (2)), from_int (-6); + (from_int (-3), from_int (3)), from_int (-9); + (from_int (-3), from_int (4)), from_int (-12); + (from_int (-3), from_int (5)), from_int (-15); + (from_int (-3), from_int (515)), from_int (-1545); + (from_int (-3), from_int (7)), from_int (-21); + (from_int (-3), from_int (9)), from_int (-27); + (from_int (-3), from_int (11)), from_int (-33); + (from_int (-3), from_int (13)), from_int (-39); + (from_int (-3), from_int (16)), from_int (-48); + (from_int (-3), from_int (17)), from_int (-51); + (from_int (-3), from_int (19)), from_int (-57); + (from_int (-3), from_int (23)), from_int (-69); + (from_int (-3), from_int (25)), from_int (-75); + (from_int (-3), from_int (29)), from_int (-87); + (from_int (-3), from_int (5026)), from_int (-15078); + (from_int (-3), from_int (5489)), from_int (-16467); + (from_int (-3), from_int (-1)), from_int (3); + (from_int (-3), from_int (-5)), from_int (15); + (from_int (-3), from_int (-4)), from_int (12); + (from_int (-3), from_int (-3)), from_int (9); + (from_int (-3), from_int (-2)), from_int (6); + (from_int (-2), from_int (0)), from_int (0); + (from_int (-2), from_int (1)), from_int (-2); + (from_int (-2), from_int (2)), from_int (-4); + (from_int (-2), from_int (3)), from_int (-6); + (from_int (-2), from_int (4)), from_int (-8); + (from_int (-2), from_int (5)), from_int (-10); + (from_int (-2), from_int (515)), from_int (-1030); + (from_int (-2), from_int (7)), from_int (-14); + (from_int (-2), from_int (9)), from_int (-18); + (from_int (-2), from_int (11)), from_int (-22); + (from_int (-2), from_int (13)), from_int (-26); + (from_int (-2), from_int (16)), from_int (-32); + (from_int (-2), from_int (17)), from_int (-34); + (from_int (-2), from_int (19)), from_int (-38); + (from_int (-2), from_int (23)), from_int (-46); + (from_int (-2), from_int (25)), from_int (-50); + (from_int (-2), from_int (29)), from_int (-58); + (from_int (-2), from_int (5026)), from_int (-10052); + (from_int (-2), from_int (5489)), from_int (-10978); + (from_int (-2), from_int (-1)), from_int (2); + (from_int (-2), from_int (-5)), from_int (10); + (from_int (-2), from_int (-4)), from_int (8); + (from_int (-2), from_int (-3)), from_int (6); + (from_int (-2), from_int (-2)), from_int (4); + ] + in + run_test template_2_1 "mult_b" mult_b t_list +;; + + +let () = + let t_list = + [ + (from_int (0), from_int (1)), from_int (0); + (from_int (0), from_int (2)), from_int (0); + (from_int (0), from_int (3)), from_int (0); + (from_int (0), from_int (4)), from_int (0); + (from_int (0), from_int (5)), from_int (0); + (from_int (0), from_int (515)), from_int (0); + (from_int (0), from_int (7)), from_int (0); + (from_int (0), from_int (9)), from_int (0); + (from_int (0), from_int (11)), from_int (0); + (from_int (0), from_int (13)), from_int (0); + (from_int (0), from_int (16)), from_int (0); + (from_int (0), from_int (17)), from_int (0); + (from_int (0), from_int (19)), from_int (0); + (from_int (0), from_int (23)), from_int (0); + (from_int (0), from_int (25)), from_int (0); + (from_int (0), from_int (29)), from_int (0); + (from_int (0), from_int (5026)), from_int (0); + (from_int (0), from_int (5489)), from_int (0); + (from_int (0), from_int (-1)), from_int (0); + (from_int (0), from_int (-5)), from_int (0); + (from_int (0), from_int (-4)), from_int (0); + (from_int (0), from_int (-3)), from_int (0); + (from_int (0), from_int (-2)), from_int (0); + (from_int (1), from_int (1)), from_int (1); + (from_int (1), from_int (2)), from_int (0); + (from_int (1), from_int (3)), from_int (0); + (from_int (1), from_int (4)), from_int (0); + (from_int (1), from_int (5)), from_int (0); + (from_int (1), from_int (515)), from_int (0); + (from_int (1), from_int (7)), from_int (0); + (from_int (1), from_int (9)), from_int (0); + (from_int (1), from_int (11)), from_int (0); + (from_int (1), from_int (13)), from_int (0); + (from_int (1), from_int (16)), from_int (0); + (from_int (1), from_int (17)), from_int (0); + (from_int (1), from_int (19)), from_int (0); + (from_int (1), from_int (23)), from_int (0); + (from_int (1), from_int (25)), from_int (0); + (from_int (1), from_int (29)), from_int (0); + (from_int (1), from_int (5026)), from_int (0); + (from_int (1), from_int (5489)), from_int (0); + (from_int (1), from_int (-1)), from_int (-1); + (from_int (1), from_int (-5)), from_int (-1); + (from_int (1), from_int (-4)), from_int (-1); + (from_int (1), from_int (-3)), from_int (-1); + (from_int (1), from_int (-2)), from_int (-1); + (from_int (2), from_int (1)), from_int (2); + (from_int (2), from_int (2)), from_int (1); + (from_int (2), from_int (3)), from_int (0); + (from_int (2), from_int (4)), from_int (0); + (from_int (2), from_int (5)), from_int (0); + (from_int (2), from_int (515)), from_int (0); + (from_int (2), from_int (7)), from_int (0); + (from_int (2), from_int (9)), from_int (0); + (from_int (2), from_int (11)), from_int (0); + (from_int (2), from_int (13)), from_int (0); + (from_int (2), from_int (16)), from_int (0); + (from_int (2), from_int (17)), from_int (0); + (from_int (2), from_int (19)), from_int (0); + (from_int (2), from_int (23)), from_int (0); + (from_int (2), from_int (25)), from_int (0); + (from_int (2), from_int (29)), from_int (0); + (from_int (2), from_int (5026)), from_int (0); + (from_int (2), from_int (5489)), from_int (0); + (from_int (2), from_int (-1)), from_int (-2); + (from_int (2), from_int (-5)), from_int (-1); + (from_int (2), from_int (-4)), from_int (-1); + (from_int (2), from_int (-3)), from_int (-1); + (from_int (2), from_int (-2)), from_int (-1); + (from_int (3), from_int (1)), from_int (3); + (from_int (3), from_int (2)), from_int (1); + (from_int (3), from_int (3)), from_int (1); + (from_int (3), from_int (4)), from_int (0); + (from_int (3), from_int (5)), from_int (0); + (from_int (3), from_int (515)), from_int (0); + (from_int (3), from_int (7)), from_int (0); + (from_int (3), from_int (9)), from_int (0); + (from_int (3), from_int (11)), from_int (0); + (from_int (3), from_int (13)), from_int (0); + (from_int (3), from_int (16)), from_int (0); + (from_int (3), from_int (17)), from_int (0); + (from_int (3), from_int (19)), from_int (0); + (from_int (3), from_int (23)), from_int (0); + (from_int (3), from_int (25)), from_int (0); + (from_int (3), from_int (29)), from_int (0); + (from_int (3), from_int (5026)), from_int (0); + (from_int (3), from_int (5489)), from_int (0); + (from_int (3), from_int (-1)), from_int (-3); + (from_int (3), from_int (-5)), from_int (-1); + (from_int (3), from_int (-4)), from_int (-1); + (from_int (3), from_int (-3)), from_int (-1); + (from_int (3), from_int (-2)), from_int (-2); + (from_int (4), from_int (1)), from_int (4); + (from_int (4), from_int (2)), from_int (2); + (from_int (4), from_int (3)), from_int (1); + (from_int (4), from_int (4)), from_int (1); + (from_int (4), from_int (5)), from_int (0); + (from_int (4), from_int (515)), from_int (0); + (from_int (4), from_int (7)), from_int (0); + (from_int (4), from_int (9)), from_int (0); + (from_int (4), from_int (11)), from_int (0); + (from_int (4), from_int (13)), from_int (0); + (from_int (4), from_int (16)), from_int (0); + (from_int (4), from_int (17)), from_int (0); + (from_int (4), from_int (19)), from_int (0); + (from_int (4), from_int (23)), from_int (0); + (from_int (4), from_int (25)), from_int (0); + (from_int (4), from_int (29)), from_int (0); + (from_int (4), from_int (5026)), from_int (0); + (from_int (4), from_int (5489)), from_int (0); + (from_int (4), from_int (-1)), from_int (-4); + (from_int (4), from_int (-5)), from_int (-1); + (from_int (4), from_int (-4)), from_int (-1); + (from_int (4), from_int (-3)), from_int (-2); + (from_int (4), from_int (-2)), from_int (-2); + (from_int (5), from_int (1)), from_int (5); + (from_int (5), from_int (2)), from_int (2); + (from_int (5), from_int (3)), from_int (1); + (from_int (5), from_int (4)), from_int (1); + (from_int (5), from_int (5)), from_int (1); + (from_int (5), from_int (515)), from_int (0); + (from_int (5), from_int (7)), from_int (0); + (from_int (5), from_int (9)), from_int (0); + (from_int (5), from_int (11)), from_int (0); + (from_int (5), from_int (13)), from_int (0); + (from_int (5), from_int (16)), from_int (0); + (from_int (5), from_int (17)), from_int (0); + (from_int (5), from_int (19)), from_int (0); + (from_int (5), from_int (23)), from_int (0); + (from_int (5), from_int (25)), from_int (0); + (from_int (5), from_int (29)), from_int (0); + (from_int (5), from_int (5026)), from_int (0); + (from_int (5), from_int (5489)), from_int (0); + (from_int (5), from_int (-1)), from_int (-5); + (from_int (5), from_int (-5)), from_int (-1); + (from_int (5), from_int (-4)), from_int (-2); + (from_int (5), from_int (-3)), from_int (-2); + (from_int (5), from_int (-2)), from_int (-3); + (from_int (515), from_int (1)), from_int (515); + (from_int (515), from_int (2)), from_int (257); + (from_int (515), from_int (3)), from_int (171); + (from_int (515), from_int (4)), from_int (128); + (from_int (515), from_int (5)), from_int (103); + (from_int (515), from_int (515)), from_int (1); + (from_int (515), from_int (7)), from_int (73); + (from_int (515), from_int (9)), from_int (57); + (from_int (515), from_int (11)), from_int (46); + (from_int (515), from_int (13)), from_int (39); + (from_int (515), from_int (16)), from_int (32); + (from_int (515), from_int (17)), from_int (30); + (from_int (515), from_int (19)), from_int (27); + (from_int (515), from_int (23)), from_int (22); + (from_int (515), from_int (25)), from_int (20); + (from_int (515), from_int (29)), from_int (17); + (from_int (515), from_int (5026)), from_int (0); + (from_int (515), from_int (5489)), from_int (0); + (from_int (515), from_int (-1)), from_int (-515); + (from_int (515), from_int (-5)), from_int (-103); + (from_int (515), from_int (-4)), from_int (-129); + (from_int (515), from_int (-3)), from_int (-172); + (from_int (515), from_int (-2)), from_int (-258); + (from_int (7), from_int (1)), from_int (7); + (from_int (7), from_int (2)), from_int (3); + (from_int (7), from_int (3)), from_int (2); + (from_int (7), from_int (4)), from_int (1); + (from_int (7), from_int (5)), from_int (1); + (from_int (7), from_int (515)), from_int (0); + (from_int (7), from_int (7)), from_int (1); + (from_int (7), from_int (9)), from_int (0); + (from_int (7), from_int (11)), from_int (0); + (from_int (7), from_int (13)), from_int (0); + (from_int (7), from_int (16)), from_int (0); + (from_int (7), from_int (17)), from_int (0); + (from_int (7), from_int (19)), from_int (0); + (from_int (7), from_int (23)), from_int (0); + (from_int (7), from_int (25)), from_int (0); + (from_int (7), from_int (29)), from_int (0); + (from_int (7), from_int (5026)), from_int (0); + (from_int (7), from_int (5489)), from_int (0); + (from_int (7), from_int (-1)), from_int (-7); + (from_int (7), from_int (-5)), from_int (-2); + (from_int (7), from_int (-4)), from_int (-2); + (from_int (7), from_int (-3)), from_int (-3); + (from_int (7), from_int (-2)), from_int (-4); + (from_int (9), from_int (1)), from_int (9); + (from_int (9), from_int (2)), from_int (4); + (from_int (9), from_int (3)), from_int (3); + (from_int (9), from_int (4)), from_int (2); + (from_int (9), from_int (5)), from_int (1); + (from_int (9), from_int (515)), from_int (0); + (from_int (9), from_int (7)), from_int (1); + (from_int (9), from_int (9)), from_int (1); + (from_int (9), from_int (11)), from_int (0); + (from_int (9), from_int (13)), from_int (0); + (from_int (9), from_int (16)), from_int (0); + (from_int (9), from_int (17)), from_int (0); + (from_int (9), from_int (19)), from_int (0); + (from_int (9), from_int (23)), from_int (0); + (from_int (9), from_int (25)), from_int (0); + (from_int (9), from_int (29)), from_int (0); + (from_int (9), from_int (5026)), from_int (0); + (from_int (9), from_int (5489)), from_int (0); + (from_int (9), from_int (-1)), from_int (-9); + (from_int (9), from_int (-5)), from_int (-2); + (from_int (9), from_int (-4)), from_int (-3); + (from_int (9), from_int (-3)), from_int (-3); + (from_int (9), from_int (-2)), from_int (-5); + (from_int (11), from_int (1)), from_int (11); + (from_int (11), from_int (2)), from_int (5); + (from_int (11), from_int (3)), from_int (3); + (from_int (11), from_int (4)), from_int (2); + (from_int (11), from_int (5)), from_int (2); + (from_int (11), from_int (515)), from_int (0); + (from_int (11), from_int (7)), from_int (1); + (from_int (11), from_int (9)), from_int (1); + (from_int (11), from_int (11)), from_int (1); + (from_int (11), from_int (13)), from_int (0); + (from_int (11), from_int (16)), from_int (0); + (from_int (11), from_int (17)), from_int (0); + (from_int (11), from_int (19)), from_int (0); + (from_int (11), from_int (23)), from_int (0); + (from_int (11), from_int (25)), from_int (0); + (from_int (11), from_int (29)), from_int (0); + (from_int (11), from_int (5026)), from_int (0); + (from_int (11), from_int (5489)), from_int (0); + (from_int (11), from_int (-1)), from_int (-11); + (from_int (11), from_int (-5)), from_int (-3); + (from_int (11), from_int (-4)), from_int (-3); + (from_int (11), from_int (-3)), from_int (-4); + (from_int (11), from_int (-2)), from_int (-6); + (from_int (13), from_int (1)), from_int (13); + (from_int (13), from_int (2)), from_int (6); + (from_int (13), from_int (3)), from_int (4); + (from_int (13), from_int (4)), from_int (3); + (from_int (13), from_int (5)), from_int (2); + (from_int (13), from_int (515)), from_int (0); + (from_int (13), from_int (7)), from_int (1); + (from_int (13), from_int (9)), from_int (1); + (from_int (13), from_int (11)), from_int (1); + (from_int (13), from_int (13)), from_int (1); + (from_int (13), from_int (16)), from_int (0); + (from_int (13), from_int (17)), from_int (0); + (from_int (13), from_int (19)), from_int (0); + (from_int (13), from_int (23)), from_int (0); + (from_int (13), from_int (25)), from_int (0); + (from_int (13), from_int (29)), from_int (0); + (from_int (13), from_int (5026)), from_int (0); + (from_int (13), from_int (5489)), from_int (0); + (from_int (13), from_int (-1)), from_int (-13); + (from_int (13), from_int (-5)), from_int (-3); + (from_int (13), from_int (-4)), from_int (-4); + (from_int (13), from_int (-3)), from_int (-5); + (from_int (13), from_int (-2)), from_int (-7); + (from_int (16), from_int (1)), from_int (16); + (from_int (16), from_int (2)), from_int (8); + (from_int (16), from_int (3)), from_int (5); + (from_int (16), from_int (4)), from_int (4); + (from_int (16), from_int (5)), from_int (3); + (from_int (16), from_int (515)), from_int (0); + (from_int (16), from_int (7)), from_int (2); + (from_int (16), from_int (9)), from_int (1); + (from_int (16), from_int (11)), from_int (1); + (from_int (16), from_int (13)), from_int (1); + (from_int (16), from_int (16)), from_int (1); + (from_int (16), from_int (17)), from_int (0); + (from_int (16), from_int (19)), from_int (0); + (from_int (16), from_int (23)), from_int (0); + (from_int (16), from_int (25)), from_int (0); + (from_int (16), from_int (29)), from_int (0); + (from_int (16), from_int (5026)), from_int (0); + (from_int (16), from_int (5489)), from_int (0); + (from_int (16), from_int (-1)), from_int (-16); + (from_int (16), from_int (-5)), from_int (-4); + (from_int (16), from_int (-4)), from_int (-4); + (from_int (16), from_int (-3)), from_int (-6); + (from_int (16), from_int (-2)), from_int (-8); + (from_int (17), from_int (1)), from_int (17); + (from_int (17), from_int (2)), from_int (8); + (from_int (17), from_int (3)), from_int (5); + (from_int (17), from_int (4)), from_int (4); + (from_int (17), from_int (5)), from_int (3); + (from_int (17), from_int (515)), from_int (0); + (from_int (17), from_int (7)), from_int (2); + (from_int (17), from_int (9)), from_int (1); + (from_int (17), from_int (11)), from_int (1); + (from_int (17), from_int (13)), from_int (1); + (from_int (17), from_int (16)), from_int (1); + (from_int (17), from_int (17)), from_int (1); + (from_int (17), from_int (19)), from_int (0); + (from_int (17), from_int (23)), from_int (0); + (from_int (17), from_int (25)), from_int (0); + (from_int (17), from_int (29)), from_int (0); + (from_int (17), from_int (5026)), from_int (0); + (from_int (17), from_int (5489)), from_int (0); + (from_int (17), from_int (-1)), from_int (-17); + (from_int (17), from_int (-5)), from_int (-4); + (from_int (17), from_int (-4)), from_int (-5); + (from_int (17), from_int (-3)), from_int (-6); + (from_int (17), from_int (-2)), from_int (-9); + (from_int (19), from_int (1)), from_int (19); + (from_int (19), from_int (2)), from_int (9); + (from_int (19), from_int (3)), from_int (6); + (from_int (19), from_int (4)), from_int (4); + (from_int (19), from_int (5)), from_int (3); + (from_int (19), from_int (515)), from_int (0); + (from_int (19), from_int (7)), from_int (2); + (from_int (19), from_int (9)), from_int (2); + (from_int (19), from_int (11)), from_int (1); + (from_int (19), from_int (13)), from_int (1); + (from_int (19), from_int (16)), from_int (1); + (from_int (19), from_int (17)), from_int (1); + (from_int (19), from_int (19)), from_int (1); + (from_int (19), from_int (23)), from_int (0); + (from_int (19), from_int (25)), from_int (0); + (from_int (19), from_int (29)), from_int (0); + (from_int (19), from_int (5026)), from_int (0); + (from_int (19), from_int (5489)), from_int (0); + (from_int (19), from_int (-1)), from_int (-19); + (from_int (19), from_int (-5)), from_int (-4); + (from_int (19), from_int (-4)), from_int (-5); + (from_int (19), from_int (-3)), from_int (-7); + (from_int (19), from_int (-2)), from_int (-10); + (from_int (23), from_int (1)), from_int (23); + (from_int (23), from_int (2)), from_int (11); + (from_int (23), from_int (3)), from_int (7); + (from_int (23), from_int (4)), from_int (5); + (from_int (23), from_int (5)), from_int (4); + (from_int (23), from_int (515)), from_int (0); + (from_int (23), from_int (7)), from_int (3); + (from_int (23), from_int (9)), from_int (2); + (from_int (23), from_int (11)), from_int (2); + (from_int (23), from_int (13)), from_int (1); + (from_int (23), from_int (16)), from_int (1); + (from_int (23), from_int (17)), from_int (1); + (from_int (23), from_int (19)), from_int (1); + (from_int (23), from_int (23)), from_int (1); + (from_int (23), from_int (25)), from_int (0); + (from_int (23), from_int (29)), from_int (0); + (from_int (23), from_int (5026)), from_int (0); + (from_int (23), from_int (5489)), from_int (0); + (from_int (23), from_int (-1)), from_int (-23); + (from_int (23), from_int (-5)), from_int (-5); + (from_int (23), from_int (-4)), from_int (-6); + (from_int (23), from_int (-3)), from_int (-8); + (from_int (23), from_int (-2)), from_int (-12); + (from_int (25), from_int (1)), from_int (25); + (from_int (25), from_int (2)), from_int (12); + (from_int (25), from_int (3)), from_int (8); + (from_int (25), from_int (4)), from_int (6); + (from_int (25), from_int (5)), from_int (5); + (from_int (25), from_int (515)), from_int (0); + (from_int (25), from_int (7)), from_int (3); + (from_int (25), from_int (9)), from_int (2); + (from_int (25), from_int (11)), from_int (2); + (from_int (25), from_int (13)), from_int (1); + (from_int (25), from_int (16)), from_int (1); + (from_int (25), from_int (17)), from_int (1); + (from_int (25), from_int (19)), from_int (1); + (from_int (25), from_int (23)), from_int (1); + (from_int (25), from_int (25)), from_int (1); + (from_int (25), from_int (29)), from_int (0); + (from_int (25), from_int (5026)), from_int (0); + (from_int (25), from_int (5489)), from_int (0); + (from_int (25), from_int (-1)), from_int (-25); + (from_int (25), from_int (-5)), from_int (-5); + (from_int (25), from_int (-4)), from_int (-7); + (from_int (25), from_int (-3)), from_int (-9); + (from_int (25), from_int (-2)), from_int (-13); + (from_int (29), from_int (1)), from_int (29); + (from_int (29), from_int (2)), from_int (14); + (from_int (29), from_int (3)), from_int (9); + (from_int (29), from_int (4)), from_int (7); + (from_int (29), from_int (5)), from_int (5); + (from_int (29), from_int (515)), from_int (0); + (from_int (29), from_int (7)), from_int (4); + (from_int (29), from_int (9)), from_int (3); + (from_int (29), from_int (11)), from_int (2); + (from_int (29), from_int (13)), from_int (2); + (from_int (29), from_int (16)), from_int (1); + (from_int (29), from_int (17)), from_int (1); + (from_int (29), from_int (19)), from_int (1); + (from_int (29), from_int (23)), from_int (1); + (from_int (29), from_int (25)), from_int (1); + (from_int (29), from_int (29)), from_int (1); + (from_int (29), from_int (5026)), from_int (0); + (from_int (29), from_int (5489)), from_int (0); + (from_int (29), from_int (-1)), from_int (-29); + (from_int (29), from_int (-5)), from_int (-6); + (from_int (29), from_int (-4)), from_int (-8); + (from_int (29), from_int (-3)), from_int (-10); + (from_int (29), from_int (-2)), from_int (-15); + (from_int (5026), from_int (1)), from_int (5026); + (from_int (5026), from_int (2)), from_int (2513); + (from_int (5026), from_int (3)), from_int (1675); + (from_int (5026), from_int (4)), from_int (1256); + (from_int (5026), from_int (5)), from_int (1005); + (from_int (5026), from_int (515)), from_int (9); + (from_int (5026), from_int (7)), from_int (718); + (from_int (5026), from_int (9)), from_int (558); + (from_int (5026), from_int (11)), from_int (456); + (from_int (5026), from_int (13)), from_int (386); + (from_int (5026), from_int (16)), from_int (314); + (from_int (5026), from_int (17)), from_int (295); + (from_int (5026), from_int (19)), from_int (264); + (from_int (5026), from_int (23)), from_int (218); + (from_int (5026), from_int (25)), from_int (201); + (from_int (5026), from_int (29)), from_int (173); + (from_int (5026), from_int (5026)), from_int (1); + (from_int (5026), from_int (5489)), from_int (0); + (from_int (5026), from_int (-1)), from_int (-5026); + (from_int (5026), from_int (-5)), from_int (-1006); + (from_int (5026), from_int (-4)), from_int (-1257); + (from_int (5026), from_int (-3)), from_int (-1676); + (from_int (5026), from_int (-2)), from_int (-2513); + (from_int (5489), from_int (1)), from_int (5489); + (from_int (5489), from_int (2)), from_int (2744); + (from_int (5489), from_int (3)), from_int (1829); + (from_int (5489), from_int (4)), from_int (1372); + (from_int (5489), from_int (5)), from_int (1097); + (from_int (5489), from_int (515)), from_int (10); + (from_int (5489), from_int (7)), from_int (784); + (from_int (5489), from_int (9)), from_int (609); + (from_int (5489), from_int (11)), from_int (499); + (from_int (5489), from_int (13)), from_int (422); + (from_int (5489), from_int (16)), from_int (343); + (from_int (5489), from_int (17)), from_int (322); + (from_int (5489), from_int (19)), from_int (288); + (from_int (5489), from_int (23)), from_int (238); + (from_int (5489), from_int (25)), from_int (219); + (from_int (5489), from_int (29)), from_int (189); + (from_int (5489), from_int (5026)), from_int (1); + (from_int (5489), from_int (5489)), from_int (1); + (from_int (5489), from_int (-1)), from_int (-5489); + (from_int (5489), from_int (-5)), from_int (-1098); + (from_int (5489), from_int (-4)), from_int (-1373); + (from_int (5489), from_int (-3)), from_int (-1830); + (from_int (5489), from_int (-2)), from_int (-2745); + (from_int (-1), from_int (1)), from_int (-1); + (from_int (-1), from_int (2)), from_int (-1); + (from_int (-1), from_int (3)), from_int (-1); + (from_int (-1), from_int (4)), from_int (-1); + (from_int (-1), from_int (5)), from_int (-1); + (from_int (-1), from_int (515)), from_int (-1); + (from_int (-1), from_int (7)), from_int (-1); + (from_int (-1), from_int (9)), from_int (-1); + (from_int (-1), from_int (11)), from_int (-1); + (from_int (-1), from_int (13)), from_int (-1); + (from_int (-1), from_int (16)), from_int (-1); + (from_int (-1), from_int (17)), from_int (-1); + (from_int (-1), from_int (19)), from_int (-1); + (from_int (-1), from_int (23)), from_int (-1); + (from_int (-1), from_int (25)), from_int (-1); + (from_int (-1), from_int (29)), from_int (-1); + (from_int (-1), from_int (5026)), from_int (-1); + (from_int (-1), from_int (5489)), from_int (-1); + (from_int (-1), from_int (-1)), from_int (1); + (from_int (-1), from_int (-5)), from_int (0); + (from_int (-1), from_int (-4)), from_int (0); + (from_int (-1), from_int (-3)), from_int (0); + (from_int (-1), from_int (-2)), from_int (0); + (from_int (-5), from_int (1)), from_int (-5); + (from_int (-5), from_int (2)), from_int (-3); + (from_int (-5), from_int (3)), from_int (-2); + (from_int (-5), from_int (4)), from_int (-2); + (from_int (-5), from_int (5)), from_int (-1); + (from_int (-5), from_int (515)), from_int (-1); + (from_int (-5), from_int (7)), from_int (-1); + (from_int (-5), from_int (9)), from_int (-1); + (from_int (-5), from_int (11)), from_int (-1); + (from_int (-5), from_int (13)), from_int (-1); + (from_int (-5), from_int (16)), from_int (-1); + (from_int (-5), from_int (17)), from_int (-1); + (from_int (-5), from_int (19)), from_int (-1); + (from_int (-5), from_int (23)), from_int (-1); + (from_int (-5), from_int (25)), from_int (-1); + (from_int (-5), from_int (29)), from_int (-1); + (from_int (-5), from_int (5026)), from_int (-1); + (from_int (-5), from_int (5489)), from_int (-1); + (from_int (-5), from_int (-1)), from_int (5); + (from_int (-5), from_int (-5)), from_int (1); + (from_int (-5), from_int (-4)), from_int (1); + (from_int (-5), from_int (-3)), from_int (1); + (from_int (-5), from_int (-2)), from_int (2); + (from_int (-4), from_int (1)), from_int (-4); + (from_int (-4), from_int (2)), from_int (-2); + (from_int (-4), from_int (3)), from_int (-2); + (from_int (-4), from_int (4)), from_int (-1); + (from_int (-4), from_int (5)), from_int (-1); + (from_int (-4), from_int (515)), from_int (-1); + (from_int (-4), from_int (7)), from_int (-1); + (from_int (-4), from_int (9)), from_int (-1); + (from_int (-4), from_int (11)), from_int (-1); + (from_int (-4), from_int (13)), from_int (-1); + (from_int (-4), from_int (16)), from_int (-1); + (from_int (-4), from_int (17)), from_int (-1); + (from_int (-4), from_int (19)), from_int (-1); + (from_int (-4), from_int (23)), from_int (-1); + (from_int (-4), from_int (25)), from_int (-1); + (from_int (-4), from_int (29)), from_int (-1); + (from_int (-4), from_int (5026)), from_int (-1); + (from_int (-4), from_int (5489)), from_int (-1); + (from_int (-4), from_int (-1)), from_int (4); + (from_int (-4), from_int (-5)), from_int (0); + (from_int (-4), from_int (-4)), from_int (1); + (from_int (-4), from_int (-3)), from_int (1); + (from_int (-4), from_int (-2)), from_int (2); + (from_int (-3), from_int (1)), from_int (-3); + (from_int (-3), from_int (2)), from_int (-2); + (from_int (-3), from_int (3)), from_int (-1); + (from_int (-3), from_int (4)), from_int (-1); + (from_int (-3), from_int (5)), from_int (-1); + (from_int (-3), from_int (515)), from_int (-1); + (from_int (-3), from_int (7)), from_int (-1); + (from_int (-3), from_int (9)), from_int (-1); + (from_int (-3), from_int (11)), from_int (-1); + (from_int (-3), from_int (13)), from_int (-1); + (from_int (-3), from_int (16)), from_int (-1); + (from_int (-3), from_int (17)), from_int (-1); + (from_int (-3), from_int (19)), from_int (-1); + (from_int (-3), from_int (23)), from_int (-1); + (from_int (-3), from_int (25)), from_int (-1); + (from_int (-3), from_int (29)), from_int (-1); + (from_int (-3), from_int (5026)), from_int (-1); + (from_int (-3), from_int (5489)), from_int (-1); + (from_int (-3), from_int (-1)), from_int (3); + (from_int (-3), from_int (-5)), from_int (0); + (from_int (-3), from_int (-4)), from_int (0); + (from_int (-3), from_int (-3)), from_int (1); + (from_int (-3), from_int (-2)), from_int (1); + (from_int (-2), from_int (1)), from_int (-2); + (from_int (-2), from_int (2)), from_int (-1); + (from_int (-2), from_int (3)), from_int (-1); + (from_int (-2), from_int (4)), from_int (-1); + (from_int (-2), from_int (5)), from_int (-1); + (from_int (-2), from_int (515)), from_int (-1); + (from_int (-2), from_int (7)), from_int (-1); + (from_int (-2), from_int (9)), from_int (-1); + (from_int (-2), from_int (11)), from_int (-1); + (from_int (-2), from_int (13)), from_int (-1); + (from_int (-2), from_int (16)), from_int (-1); + (from_int (-2), from_int (17)), from_int (-1); + (from_int (-2), from_int (19)), from_int (-1); + (from_int (-2), from_int (23)), from_int (-1); + (from_int (-2), from_int (25)), from_int (-1); + (from_int (-2), from_int (29)), from_int (-1); + (from_int (-2), from_int (5026)), from_int (-1); + (from_int (-2), from_int (5489)), from_int (-1); + (from_int (-2), from_int (-1)), from_int (2); + (from_int (-2), from_int (-5)), from_int (0); + (from_int (-2), from_int (-4)), from_int (0); + (from_int (-2), from_int (-3)), from_int (0); + (from_int (-2), from_int (-2)), from_int (1); + ] + in + run_test template_2_1 "quot_b" quot_b t_list +;; + + +let () = + let t_list = + [ + (from_int (0), from_int (1)), from_int (0); + (from_int (0), from_int (2)), from_int (0); + (from_int (0), from_int (3)), from_int (0); + (from_int (0), from_int (4)), from_int (0); + (from_int (0), from_int (5)), from_int (0); + (from_int (0), from_int (515)), from_int (0); + (from_int (0), from_int (7)), from_int (0); + (from_int (0), from_int (9)), from_int (0); + (from_int (0), from_int (11)), from_int (0); + (from_int (0), from_int (13)), from_int (0); + (from_int (0), from_int (16)), from_int (0); + (from_int (0), from_int (17)), from_int (0); + (from_int (0), from_int (19)), from_int (0); + (from_int (0), from_int (23)), from_int (0); + (from_int (0), from_int (25)), from_int (0); + (from_int (0), from_int (29)), from_int (0); + (from_int (0), from_int (5026)), from_int (0); + (from_int (0), from_int (5489)), from_int (0); + (from_int (1), from_int (1)), from_int (0); + (from_int (1), from_int (2)), from_int (1); + (from_int (1), from_int (3)), from_int (1); + (from_int (1), from_int (4)), from_int (1); + (from_int (1), from_int (5)), from_int (1); + (from_int (1), from_int (515)), from_int (1); + (from_int (1), from_int (7)), from_int (1); + (from_int (1), from_int (9)), from_int (1); + (from_int (1), from_int (11)), from_int (1); + (from_int (1), from_int (13)), from_int (1); + (from_int (1), from_int (16)), from_int (1); + (from_int (1), from_int (17)), from_int (1); + (from_int (1), from_int (19)), from_int (1); + (from_int (1), from_int (23)), from_int (1); + (from_int (1), from_int (25)), from_int (1); + (from_int (1), from_int (29)), from_int (1); + (from_int (1), from_int (5026)), from_int (1); + (from_int (1), from_int (5489)), from_int (1); + (from_int (2), from_int (1)), from_int (0); + (from_int (2), from_int (2)), from_int (0); + (from_int (2), from_int (3)), from_int (2); + (from_int (2), from_int (4)), from_int (2); + (from_int (2), from_int (5)), from_int (2); + (from_int (2), from_int (515)), from_int (2); + (from_int (2), from_int (7)), from_int (2); + (from_int (2), from_int (9)), from_int (2); + (from_int (2), from_int (11)), from_int (2); + (from_int (2), from_int (13)), from_int (2); + (from_int (2), from_int (16)), from_int (2); + (from_int (2), from_int (17)), from_int (2); + (from_int (2), from_int (19)), from_int (2); + (from_int (2), from_int (23)), from_int (2); + (from_int (2), from_int (25)), from_int (2); + (from_int (2), from_int (29)), from_int (2); + (from_int (2), from_int (5026)), from_int (2); + (from_int (2), from_int (5489)), from_int (2); + (from_int (3), from_int (1)), from_int (0); + (from_int (3), from_int (2)), from_int (1); + (from_int (3), from_int (3)), from_int (0); + (from_int (3), from_int (4)), from_int (3); + (from_int (3), from_int (5)), from_int (3); + (from_int (3), from_int (515)), from_int (3); + (from_int (3), from_int (7)), from_int (3); + (from_int (3), from_int (9)), from_int (3); + (from_int (3), from_int (11)), from_int (3); + (from_int (3), from_int (13)), from_int (3); + (from_int (3), from_int (16)), from_int (3); + (from_int (3), from_int (17)), from_int (3); + (from_int (3), from_int (19)), from_int (3); + (from_int (3), from_int (23)), from_int (3); + (from_int (3), from_int (25)), from_int (3); + (from_int (3), from_int (29)), from_int (3); + (from_int (3), from_int (5026)), from_int (3); + (from_int (3), from_int (5489)), from_int (3); + (from_int (4), from_int (1)), from_int (0); + (from_int (4), from_int (2)), from_int (0); + (from_int (4), from_int (3)), from_int (1); + (from_int (4), from_int (4)), from_int (0); + (from_int (4), from_int (5)), from_int (4); + (from_int (4), from_int (515)), from_int (4); + (from_int (4), from_int (7)), from_int (4); + (from_int (4), from_int (9)), from_int (4); + (from_int (4), from_int (11)), from_int (4); + (from_int (4), from_int (13)), from_int (4); + (from_int (4), from_int (16)), from_int (4); + (from_int (4), from_int (17)), from_int (4); + (from_int (4), from_int (19)), from_int (4); + (from_int (4), from_int (23)), from_int (4); + (from_int (4), from_int (25)), from_int (4); + (from_int (4), from_int (29)), from_int (4); + (from_int (4), from_int (5026)), from_int (4); + (from_int (4), from_int (5489)), from_int (4); + (from_int (5), from_int (1)), from_int (0); + (from_int (5), from_int (2)), from_int (1); + (from_int (5), from_int (3)), from_int (2); + (from_int (5), from_int (4)), from_int (1); + (from_int (5), from_int (5)), from_int (0); + (from_int (5), from_int (515)), from_int (5); + (from_int (5), from_int (7)), from_int (5); + (from_int (5), from_int (9)), from_int (5); + (from_int (5), from_int (11)), from_int (5); + (from_int (5), from_int (13)), from_int (5); + (from_int (5), from_int (16)), from_int (5); + (from_int (5), from_int (17)), from_int (5); + (from_int (5), from_int (19)), from_int (5); + (from_int (5), from_int (23)), from_int (5); + (from_int (5), from_int (25)), from_int (5); + (from_int (5), from_int (29)), from_int (5); + (from_int (5), from_int (5026)), from_int (5); + (from_int (5), from_int (5489)), from_int (5); + (from_int (515), from_int (1)), from_int (0); + (from_int (515), from_int (2)), from_int (1); + (from_int (515), from_int (3)), from_int (2); + (from_int (515), from_int (4)), from_int (3); + (from_int (515), from_int (5)), from_int (0); + (from_int (515), from_int (515)), from_int (0); + (from_int (515), from_int (7)), from_int (4); + (from_int (515), from_int (9)), from_int (2); + (from_int (515), from_int (11)), from_int (9); + (from_int (515), from_int (13)), from_int (8); + (from_int (515), from_int (16)), from_int (3); + (from_int (515), from_int (17)), from_int (5); + (from_int (515), from_int (19)), from_int (2); + (from_int (515), from_int (23)), from_int (9); + (from_int (515), from_int (25)), from_int (15); + (from_int (515), from_int (29)), from_int (22); + (from_int (515), from_int (5026)), from_int (515); + (from_int (515), from_int (5489)), from_int (515); + (from_int (7), from_int (1)), from_int (0); + (from_int (7), from_int (2)), from_int (1); + (from_int (7), from_int (3)), from_int (1); + (from_int (7), from_int (4)), from_int (3); + (from_int (7), from_int (5)), from_int (2); + (from_int (7), from_int (515)), from_int (7); + (from_int (7), from_int (7)), from_int (0); + (from_int (7), from_int (9)), from_int (7); + (from_int (7), from_int (11)), from_int (7); + (from_int (7), from_int (13)), from_int (7); + (from_int (7), from_int (16)), from_int (7); + (from_int (7), from_int (17)), from_int (7); + (from_int (7), from_int (19)), from_int (7); + (from_int (7), from_int (23)), from_int (7); + (from_int (7), from_int (25)), from_int (7); + (from_int (7), from_int (29)), from_int (7); + (from_int (7), from_int (5026)), from_int (7); + (from_int (7), from_int (5489)), from_int (7); + (from_int (9), from_int (1)), from_int (0); + (from_int (9), from_int (2)), from_int (1); + (from_int (9), from_int (3)), from_int (0); + (from_int (9), from_int (4)), from_int (1); + (from_int (9), from_int (5)), from_int (4); + (from_int (9), from_int (515)), from_int (9); + (from_int (9), from_int (7)), from_int (2); + (from_int (9), from_int (9)), from_int (0); + (from_int (9), from_int (11)), from_int (9); + (from_int (9), from_int (13)), from_int (9); + (from_int (9), from_int (16)), from_int (9); + (from_int (9), from_int (17)), from_int (9); + (from_int (9), from_int (19)), from_int (9); + (from_int (9), from_int (23)), from_int (9); + (from_int (9), from_int (25)), from_int (9); + (from_int (9), from_int (29)), from_int (9); + (from_int (9), from_int (5026)), from_int (9); + (from_int (9), from_int (5489)), from_int (9); + (from_int (11), from_int (1)), from_int (0); + (from_int (11), from_int (2)), from_int (1); + (from_int (11), from_int (3)), from_int (2); + (from_int (11), from_int (4)), from_int (3); + (from_int (11), from_int (5)), from_int (1); + (from_int (11), from_int (515)), from_int (11); + (from_int (11), from_int (7)), from_int (4); + (from_int (11), from_int (9)), from_int (2); + (from_int (11), from_int (11)), from_int (0); + (from_int (11), from_int (13)), from_int (11); + (from_int (11), from_int (16)), from_int (11); + (from_int (11), from_int (17)), from_int (11); + (from_int (11), from_int (19)), from_int (11); + (from_int (11), from_int (23)), from_int (11); + (from_int (11), from_int (25)), from_int (11); + (from_int (11), from_int (29)), from_int (11); + (from_int (11), from_int (5026)), from_int (11); + (from_int (11), from_int (5489)), from_int (11); + (from_int (13), from_int (1)), from_int (0); + (from_int (13), from_int (2)), from_int (1); + (from_int (13), from_int (3)), from_int (1); + (from_int (13), from_int (4)), from_int (1); + (from_int (13), from_int (5)), from_int (3); + (from_int (13), from_int (515)), from_int (13); + (from_int (13), from_int (7)), from_int (6); + (from_int (13), from_int (9)), from_int (4); + (from_int (13), from_int (11)), from_int (2); + (from_int (13), from_int (13)), from_int (0); + (from_int (13), from_int (16)), from_int (13); + (from_int (13), from_int (17)), from_int (13); + (from_int (13), from_int (19)), from_int (13); + (from_int (13), from_int (23)), from_int (13); + (from_int (13), from_int (25)), from_int (13); + (from_int (13), from_int (29)), from_int (13); + (from_int (13), from_int (5026)), from_int (13); + (from_int (13), from_int (5489)), from_int (13); + (from_int (16), from_int (1)), from_int (0); + (from_int (16), from_int (2)), from_int (0); + (from_int (16), from_int (3)), from_int (1); + (from_int (16), from_int (4)), from_int (0); + (from_int (16), from_int (5)), from_int (1); + (from_int (16), from_int (515)), from_int (16); + (from_int (16), from_int (7)), from_int (2); + (from_int (16), from_int (9)), from_int (7); + (from_int (16), from_int (11)), from_int (5); + (from_int (16), from_int (13)), from_int (3); + (from_int (16), from_int (16)), from_int (0); + (from_int (16), from_int (17)), from_int (16); + (from_int (16), from_int (19)), from_int (16); + (from_int (16), from_int (23)), from_int (16); + (from_int (16), from_int (25)), from_int (16); + (from_int (16), from_int (29)), from_int (16); + (from_int (16), from_int (5026)), from_int (16); + (from_int (16), from_int (5489)), from_int (16); + (from_int (17), from_int (1)), from_int (0); + (from_int (17), from_int (2)), from_int (1); + (from_int (17), from_int (3)), from_int (2); + (from_int (17), from_int (4)), from_int (1); + (from_int (17), from_int (5)), from_int (2); + (from_int (17), from_int (515)), from_int (17); + (from_int (17), from_int (7)), from_int (3); + (from_int (17), from_int (9)), from_int (8); + (from_int (17), from_int (11)), from_int (6); + (from_int (17), from_int (13)), from_int (4); + (from_int (17), from_int (16)), from_int (1); + (from_int (17), from_int (17)), from_int (0); + (from_int (17), from_int (19)), from_int (17); + (from_int (17), from_int (23)), from_int (17); + (from_int (17), from_int (25)), from_int (17); + (from_int (17), from_int (29)), from_int (17); + (from_int (17), from_int (5026)), from_int (17); + (from_int (17), from_int (5489)), from_int (17); + (from_int (19), from_int (1)), from_int (0); + (from_int (19), from_int (2)), from_int (1); + (from_int (19), from_int (3)), from_int (1); + (from_int (19), from_int (4)), from_int (3); + (from_int (19), from_int (5)), from_int (4); + (from_int (19), from_int (515)), from_int (19); + (from_int (19), from_int (7)), from_int (5); + (from_int (19), from_int (9)), from_int (1); + (from_int (19), from_int (11)), from_int (8); + (from_int (19), from_int (13)), from_int (6); + (from_int (19), from_int (16)), from_int (3); + (from_int (19), from_int (17)), from_int (2); + (from_int (19), from_int (19)), from_int (0); + (from_int (19), from_int (23)), from_int (19); + (from_int (19), from_int (25)), from_int (19); + (from_int (19), from_int (29)), from_int (19); + (from_int (19), from_int (5026)), from_int (19); + (from_int (19), from_int (5489)), from_int (19); + (from_int (23), from_int (1)), from_int (0); + (from_int (23), from_int (2)), from_int (1); + (from_int (23), from_int (3)), from_int (2); + (from_int (23), from_int (4)), from_int (3); + (from_int (23), from_int (5)), from_int (3); + (from_int (23), from_int (515)), from_int (23); + (from_int (23), from_int (7)), from_int (2); + (from_int (23), from_int (9)), from_int (5); + (from_int (23), from_int (11)), from_int (1); + (from_int (23), from_int (13)), from_int (10); + (from_int (23), from_int (16)), from_int (7); + (from_int (23), from_int (17)), from_int (6); + (from_int (23), from_int (19)), from_int (4); + (from_int (23), from_int (23)), from_int (0); + (from_int (23), from_int (25)), from_int (23); + (from_int (23), from_int (29)), from_int (23); + (from_int (23), from_int (5026)), from_int (23); + (from_int (23), from_int (5489)), from_int (23); + (from_int (25), from_int (1)), from_int (0); + (from_int (25), from_int (2)), from_int (1); + (from_int (25), from_int (3)), from_int (1); + (from_int (25), from_int (4)), from_int (1); + (from_int (25), from_int (5)), from_int (0); + (from_int (25), from_int (515)), from_int (25); + (from_int (25), from_int (7)), from_int (4); + (from_int (25), from_int (9)), from_int (7); + (from_int (25), from_int (11)), from_int (3); + (from_int (25), from_int (13)), from_int (12); + (from_int (25), from_int (16)), from_int (9); + (from_int (25), from_int (17)), from_int (8); + (from_int (25), from_int (19)), from_int (6); + (from_int (25), from_int (23)), from_int (2); + (from_int (25), from_int (25)), from_int (0); + (from_int (25), from_int (29)), from_int (25); + (from_int (25), from_int (5026)), from_int (25); + (from_int (25), from_int (5489)), from_int (25); + (from_int (29), from_int (1)), from_int (0); + (from_int (29), from_int (2)), from_int (1); + (from_int (29), from_int (3)), from_int (2); + (from_int (29), from_int (4)), from_int (1); + (from_int (29), from_int (5)), from_int (4); + (from_int (29), from_int (515)), from_int (29); + (from_int (29), from_int (7)), from_int (1); + (from_int (29), from_int (9)), from_int (2); + (from_int (29), from_int (11)), from_int (7); + (from_int (29), from_int (13)), from_int (3); + (from_int (29), from_int (16)), from_int (13); + (from_int (29), from_int (17)), from_int (12); + (from_int (29), from_int (19)), from_int (10); + (from_int (29), from_int (23)), from_int (6); + (from_int (29), from_int (25)), from_int (4); + (from_int (29), from_int (29)), from_int (0); + (from_int (29), from_int (5026)), from_int (29); + (from_int (29), from_int (5489)), from_int (29); + (from_int (5026), from_int (1)), from_int (0); + (from_int (5026), from_int (2)), from_int (0); + (from_int (5026), from_int (3)), from_int (1); + (from_int (5026), from_int (4)), from_int (2); + (from_int (5026), from_int (5)), from_int (1); + (from_int (5026), from_int (515)), from_int (391); + (from_int (5026), from_int (7)), from_int (0); + (from_int (5026), from_int (9)), from_int (4); + (from_int (5026), from_int (11)), from_int (10); + (from_int (5026), from_int (13)), from_int (8); + (from_int (5026), from_int (16)), from_int (2); + (from_int (5026), from_int (17)), from_int (11); + (from_int (5026), from_int (19)), from_int (10); + (from_int (5026), from_int (23)), from_int (12); + (from_int (5026), from_int (25)), from_int (1); + (from_int (5026), from_int (29)), from_int (9); + (from_int (5026), from_int (5026)), from_int (0); + (from_int (5026), from_int (5489)), from_int (5026); + (from_int (5489), from_int (1)), from_int (0); + (from_int (5489), from_int (2)), from_int (1); + (from_int (5489), from_int (3)), from_int (2); + (from_int (5489), from_int (4)), from_int (1); + (from_int (5489), from_int (5)), from_int (4); + (from_int (5489), from_int (515)), from_int (339); + (from_int (5489), from_int (7)), from_int (1); + (from_int (5489), from_int (9)), from_int (8); + (from_int (5489), from_int (11)), from_int (0); + (from_int (5489), from_int (13)), from_int (3); + (from_int (5489), from_int (16)), from_int (1); + (from_int (5489), from_int (17)), from_int (15); + (from_int (5489), from_int (19)), from_int (17); + (from_int (5489), from_int (23)), from_int (15); + (from_int (5489), from_int (25)), from_int (14); + (from_int (5489), from_int (29)), from_int (8); + (from_int (5489), from_int (5026)), from_int (463); + (from_int (5489), from_int (5489)), from_int (0); + (from_int (-1), from_int (1)), from_int (0); + (from_int (-1), from_int (2)), from_int (1); + (from_int (-1), from_int (3)), from_int (2); + (from_int (-1), from_int (4)), from_int (3); + (from_int (-1), from_int (5)), from_int (4); + (from_int (-1), from_int (515)), from_int (514); + (from_int (-1), from_int (7)), from_int (6); + (from_int (-1), from_int (9)), from_int (8); + (from_int (-1), from_int (11)), from_int (10); + (from_int (-1), from_int (13)), from_int (12); + (from_int (-1), from_int (16)), from_int (15); + (from_int (-1), from_int (17)), from_int (16); + (from_int (-1), from_int (19)), from_int (18); + (from_int (-1), from_int (23)), from_int (22); + (from_int (-1), from_int (25)), from_int (24); + (from_int (-1), from_int (29)), from_int (28); + (from_int (-1), from_int (5026)), from_int (5025); + (from_int (-1), from_int (5489)), from_int (5488); + (from_int (-5), from_int (1)), from_int (0); + (from_int (-5), from_int (2)), from_int (1); + (from_int (-5), from_int (3)), from_int (1); + (from_int (-5), from_int (4)), from_int (3); + (from_int (-5), from_int (5)), from_int (0); + (from_int (-5), from_int (515)), from_int (510); + (from_int (-5), from_int (7)), from_int (2); + (from_int (-5), from_int (9)), from_int (4); + (from_int (-5), from_int (11)), from_int (6); + (from_int (-5), from_int (13)), from_int (8); + (from_int (-5), from_int (16)), from_int (11); + (from_int (-5), from_int (17)), from_int (12); + (from_int (-5), from_int (19)), from_int (14); + (from_int (-5), from_int (23)), from_int (18); + (from_int (-5), from_int (25)), from_int (20); + (from_int (-5), from_int (29)), from_int (24); + (from_int (-5), from_int (5026)), from_int (5021); + (from_int (-5), from_int (5489)), from_int (5484); + (from_int (-4), from_int (1)), from_int (0); + (from_int (-4), from_int (2)), from_int (0); + (from_int (-4), from_int (3)), from_int (2); + (from_int (-4), from_int (4)), from_int (0); + (from_int (-4), from_int (5)), from_int (1); + (from_int (-4), from_int (515)), from_int (511); + (from_int (-4), from_int (7)), from_int (3); + (from_int (-4), from_int (9)), from_int (5); + (from_int (-4), from_int (11)), from_int (7); + (from_int (-4), from_int (13)), from_int (9); + (from_int (-4), from_int (16)), from_int (12); + (from_int (-4), from_int (17)), from_int (13); + (from_int (-4), from_int (19)), from_int (15); + (from_int (-4), from_int (23)), from_int (19); + (from_int (-4), from_int (25)), from_int (21); + (from_int (-4), from_int (29)), from_int (25); + (from_int (-4), from_int (5026)), from_int (5022); + (from_int (-4), from_int (5489)), from_int (5485); + (from_int (-3), from_int (1)), from_int (0); + (from_int (-3), from_int (2)), from_int (1); + (from_int (-3), from_int (3)), from_int (0); + (from_int (-3), from_int (4)), from_int (1); + (from_int (-3), from_int (5)), from_int (2); + (from_int (-3), from_int (515)), from_int (512); + (from_int (-3), from_int (7)), from_int (4); + (from_int (-3), from_int (9)), from_int (6); + (from_int (-3), from_int (11)), from_int (8); + (from_int (-3), from_int (13)), from_int (10); + (from_int (-3), from_int (16)), from_int (13); + (from_int (-3), from_int (17)), from_int (14); + (from_int (-3), from_int (19)), from_int (16); + (from_int (-3), from_int (23)), from_int (20); + (from_int (-3), from_int (25)), from_int (22); + (from_int (-3), from_int (29)), from_int (26); + (from_int (-3), from_int (5026)), from_int (5023); + (from_int (-3), from_int (5489)), from_int (5486); + (from_int (-2), from_int (1)), from_int (0); + (from_int (-2), from_int (2)), from_int (0); + (from_int (-2), from_int (3)), from_int (1); + (from_int (-2), from_int (4)), from_int (2); + (from_int (-2), from_int (5)), from_int (3); + (from_int (-2), from_int (515)), from_int (513); + (from_int (-2), from_int (7)), from_int (5); + (from_int (-2), from_int (9)), from_int (7); + (from_int (-2), from_int (11)), from_int (9); + (from_int (-2), from_int (13)), from_int (11); + (from_int (-2), from_int (16)), from_int (14); + (from_int (-2), from_int (17)), from_int (15); + (from_int (-2), from_int (19)), from_int (17); + (from_int (-2), from_int (23)), from_int (21); + (from_int (-2), from_int (25)), from_int (23); + (from_int (-2), from_int (29)), from_int (27); + (from_int (-2), from_int (5026)), from_int (5024); + (from_int (-2), from_int (5489)), from_int (5487); + ] + in + run_test template_2_1 "mod_b" mod_b t_list +;; \ No newline at end of file diff --git a/Source/scalable/tests/test_scalable_ciphers.ml b/Source/scalable/tests/test_scalable_ciphers.ml index e6008ca..70b51fb 100644 --- a/Source/scalable/tests/test_scalable_ciphers.ml +++ b/Source/scalable/tests/test_scalable_ciphers.ml @@ -11,8 +11,8 @@ open Test_scalable_templates let p = from_int 9967 and q = from_int 9973 let ((_, e), (n, d)) = generate_keys_rsa p q -let phin = mult_b (diff_b p [1;1]) (diff_b q [1;1]) -let is_inverse x y n = mod_b (mult_b (mod_b x n) (mod_b y n)) n = [1; 1] +let phin = mult_b (diff_b p [0;1]) (diff_b q [0;1]) +let is_inverse x y n = mod_b (mult_b (mod_b x n) (mod_b y n)) n = [0; 1] let () = let t_list = [(e, d, phin), true] in run_test template_3_b "Generate RSA Keys Test" is_inverse t_list