1.1 --- a/test/Tools/isac/Knowledge/gcd_poly_ml.sml	Sun Sep 01 15:54:48 2013 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/gcd_poly_ml.sml	Sun Sep 01 16:50:51 2013 +0200
     1.3 @@ -804,10 +804,16 @@
     1.4  if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "gcd_poly mail changed";
     1.5  (* \<forall>c'. (c' dvd\<^isub>p  a \<and> c' dvd\<^isub>p b) \<longrightarrow> c' \<le>\<^isub>p c) can NOT be checked this way, of course *)
     1.6  
     1.7 +(* regression test for --- fun gcd_poly downto division by zero ---*)
     1.8 +val a = [(9, [5, 2, 4])]: poly
     1.9 +val b = [(15, [6, 3, 1])]: poly
    1.10 +val ((a', b'), c) = gcd_poly a b;
    1.11 +if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "regression test changed";
    1.12 +
    1.13  "----------- fun gcd_poly downto division by zero -------";
    1.14  "----------- fun gcd_poly downto division by zero -------";
    1.15  "----------- fun gcd_poly downto division by zero -------";
    1.16 -"-------- example 187a: exception Div raised...";
    1.17 +"-------- example 187a: exception Div raised...  REGRSSION TEST FOR REMOVAL OF THIS BUG IS ABOVE";
    1.18  val a = [(12, [1, 1])]: poly
    1.19  val b = [(8, [0, 2])]: poly;
    1.20  (*            val ((a', b'), c) = gcd_poly a b