alt-ergo crash - Githubissues

Hi,

Alt-ergo crash when run on the files dumped at the bottom. The following error is reported:

Fatal error: exception Assert_failure("src/theories/ac.ml", 161, 17)

It does not seem to be easily reproducible: those files were generated by Why3 together with a lot of other similar files but only those two caused the crash.

Regards,

Martin Clochard.

File 1(394 lines)

(* this is a prelude for Alt-Ergo) ( this is a prelude for Alt-Ergo integer arithmetic *) logic safe_comp_div: int, int -> int axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y logic safe_comp_mod: int, int -> int axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y logic safe_eucl_div: int, int -> int axiom safe_eucl_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_div(x,y) = x / y logic safe_eucl_mod: int, int -> int axiom safe_eucl_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_mod(x,y) = x % y logic match_bool : bool, 'a, 'a -> 'a

axiom match_bool_True : (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))

axiom match_bool_False : (forall z:'a. forall z1:'a. (match_bool(false, z, z1) = z1))

axiom CompatOrderMult1 : (forall x:int. forall y:int. forall z:int. ((x <= y) -> ((0 <= z) -> ((x * z) <= (y * z)))))

logic abs1 : int -> int

axiom abs_def2 : (forall x:int. ((0 <= x) -> (abs1(x) = x)))

axiom abs_def3 : (forall x:int. ((not (0 <= x)) -> (abs1(x) = (-x))))

axiom Abs_le3 : (forall x:int. forall y:int. ((abs1(x) <= y) -> ((-y) <= x)))

axiom Abs_le4 : (forall x:int. forall y:int. ((abs1(x) <= y) -> (x <= y)))

axiom Abs_le5 : (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) -> (abs1(x) <= y)))

axiom Abs_pos1 : (forall x:int. (0 <= abs1(x)))

axiom Div_mod2 : (forall x:int. forall y:int. ((not (y = 0)) -> (x = ((y * safe_comp_div(x,y)) + safe_comp_mod(x,y)))))

axiom Div_bound4 : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (0 <= safe_comp_div(x,y))))

axiom Div_bound5 : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (safe_comp_div(x,y) <= x)))

axiom Mod_bound4 : (forall x:int. forall y:int. ((not (y = 0)) -> ((-abs1(y)) < safe_comp_mod(x,y))))

axiom Mod_bound5 : (forall x:int. forall y:int. ((not (y = 0)) -> (safe_comp_mod(x,y) < abs1(y))))

axiom Div_sign_pos1 : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (0 <= safe_comp_div(x,y))))

axiom Div_sign_neg1 : (forall x:int. forall y:int. (((x <= 0) and (0 < y)) -> (safe_comp_div(x,y) <= 0)))

axiom Mod_sign_pos1 : (forall x:int. forall y:int. (((0 <= x) and (not (y = 0))) -> (0 <= safe_comp_mod(x,y))))

axiom Mod_sign_neg1 : (forall x:int. forall y:int. (((x <= 0) and (not (y = 0))) -> (safe_comp_mod(x,y) <= 0)))

axiom Rounds_toward_zero1 : (forall x:int. forall y:int. ((not (y = 0)) -> (abs1((safe_comp_div(x,y) * y)) <= abs1(x))))

axiom Div_12 : (forall x:int. (safe_comp_div(x,1) = x))

axiom Mod_12 : (forall x:int. (safe_comp_mod(x,1) = 0))

axiom Div_inf2 : (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> (safe_comp_div(x,y) = 0)))

axiom Mod_inf1 : (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> (safe_comp_mod(x,y) = x)))

axiom Div_mult2 : (forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)]. (((0 < x) and ((0 <= y) and (0 <= z))) -> (safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x)))))

axiom Mod_mult2 : (forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)]. (((0 < x) and ((0 <= y) and (0 <= z))) -> (safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x))))

predicate divides1(d: int, n: int) = (exists q:int. (n = (q * d)))

axiom divides_refl1 : (forall n:int. divides1(n, n))

axiom divides_1_n1 : (forall n:int. divides1(1, n))

axiom divides_01 : (forall n:int. divides1(n, 0))

axiom divides_left1 : (forall a:int. forall b:int. forall c:int. (divides1(a, b) -> divides1((c * a), (c * b))))

axiom divides_right1 : (forall a:int. forall b:int. forall c:int. (divides1(a, b) -> divides1((a * c), (b * c))))

axiom divides_oppr1 : (forall a:int. forall b:int. (divides1(a, b) -> divides1(a, (-b))))

axiom divides_oppl1 : (forall a:int. forall b:int. (divides1(a, b) -> divides1((-a), b)))

axiom divides_oppr_rev1 : (forall a:int. forall b:int. (divides1((-a), b) -> divides1(a, b)))

axiom divides_oppl_rev1 : (forall a:int. forall b:int. (divides1(a, (-b)) -> divides1(a, b)))

axiom divides_plusr1 : (forall a:int. forall b:int. forall c:int. (divides1(a, b) -> (divides1(a, c) -> divides1(a, (b + c)))))

axiom divides_minusr1 : (forall a:int. forall b:int. forall c:int. (divides1(a, b) -> (divides1(a, c) -> divides1(a, (b - c)))))

axiom divides_multl1 : (forall a:int. forall b:int. forall c:int. (divides1(a, b) -> divides1(a, (c * b))))

axiom divides_multr1 : (forall a:int. forall b:int. forall c:int. (divides1(a, b) -> divides1(a, (b * c))))

axiom divides_factorl1 : (forall a:int. forall b:int. divides1(a, (b * a)))

axiom divides_factorr1 : (forall a:int. forall b:int. divides1(a, (a * b)))

axiom divides_n_11 : (forall n:int. (divides1(n, 1) -> ((n = 1) or (n = (-1)))))

axiom divides_antisym1 : (forall a:int. forall b:int. (divides1(a, b) -> (divides1(b, a) -> ((a = b) or (a = (-b))))))

axiom divides_trans1 : (forall a:int. forall b:int. forall c:int. (divides1(a, b) -> (divides1(b, c) -> divides1(a, c))))

axiom divides_bounds1 : (forall a:int. forall b:int. (divides1(a, b) -> ((not (b = 0)) -> (abs1(a) <= abs1(b)))))

axiom Div_mod3 : (forall x:int. forall y:int. ((not (y = 0)) -> (x = ((y * safe_eucl_div(x,y)) + safe_eucl_mod(x,y)))))

axiom Div_bound6 : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (0 <= safe_eucl_div(x,y))))

axiom Div_bound7 : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (safe_eucl_div(x,y) <= x)))

axiom Mod_bound6 : (forall x:int. forall y:int. ((not (y = 0)) -> (0 <= safe_eucl_mod(x,y))))

axiom Mod_bound7 : (forall x:int. forall y:int. ((not (y = 0)) -> (safe_eucl_mod(x,y) < abs1(y))))

axiom Mod_13 : (forall x:int. (safe_eucl_mod(x,1) = 0))

axiom Div_13 : (forall x:int. (safe_eucl_div(x,1) = x))

axiom Div_inf3 : (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> (safe_eucl_div(x,y) = 0)))

axiom Div_inf_neg1 : (forall x:int. forall y:int. (((0 < x) and (x <= y)) -> (safe_eucl_div((-x),y) = (-1))))

axiom Mod_01 : (forall y:int. ((not (y = 0)) -> (safe_eucl_mod(0,y) = 0)))

axiom Div_1_left1 : (forall y:int. ((1 < y) -> (safe_eucl_div(1,y) = 0)))

axiom Div_minus1_left1 : (forall y:int. ((1 < y) -> (safe_eucl_div((-1),y) = (-1))))

axiom Mod_1_left1 : (forall y:int. ((1 < y) -> (safe_eucl_mod(1,y) = 1)))

axiom Mod_minus1_left1 : (forall y:int. ((1 < y) -> (safe_eucl_mod((-1),y) = (y - 1))))

axiom Div_mult3 : (forall x:int. forall y:int. forall z:int [safe_eucl_div(((x * y) + z),x)]. ((0 < x) -> (safe_eucl_div(((x * y) + z),x) = (y + safe_eucl_div(z,x)))))

axiom Mod_mult3 : (forall x:int. forall y:int. forall z:int [safe_eucl_mod(((x * y) + z),x)]. ((0 < x) -> (safe_eucl_mod(((x * y) + z),x) = safe_eucl_mod(z,x))))

axiom mod_divides_euclidean1 : (forall a:int. forall b:int. ((not (b = 0)) -> ((safe_eucl_mod(a,b) = 0) -> divides1(b, a))))

axiom divides_mod_euclidean1 : (forall a:int. forall b:int. ((not (b = 0)) -> (divides1(b, a) -> (safe_eucl_mod(a,b) = 0))))

axiom mod_divides_computer1 : (forall a:int. forall b:int. ((not (b = 0)) -> ((safe_comp_mod(a,b) = 0) -> divides1(b, a))))

axiom divides_mod_computer1 : (forall a:int. forall b:int. ((not (b = 0)) -> (divides1(b, a) -> (safe_comp_mod(a,b) = 0))))

predicate even1(n: int) = (exists k:int. (n = (2 * k)))

predicate odd1(n: int) = (exists k:int. (n = ((2 * k) + 1)))

axiom even_or_odd1 : (forall n:int. (even1(n) or odd1(n)))

axiom even_not_odd1 : (forall n:int. (even1(n) -> (not odd1(n))))

axiom odd_not_even1 : (forall n:int. (odd1(n) -> (not even1(n))))

axiom even_odd1 : (forall n:int. (even1(n) -> odd1((n + 1))))

axiom odd_even1 : (forall n:int. (odd1(n) -> even1((n + 1))))

axiom even_even1 : (forall n:int. (even1(n) -> even1((n + 2))))

axiom odd_odd1 : (forall n:int. (odd1(n) -> odd1((n + 2))))

axiom even_2k1 : (forall k:int. even1((2 * k)))

axiom odd_2k11 : (forall k:int. odd1(((2 * k) + 1)))

axiom even_divides2 : (forall a:int. (even1(a) -> divides1(2, a)))

axiom even_divides3 : (forall a:int. (divides1(2, a) -> even1(a)))

axiom odd_divides2 : (forall a:int. (odd1(a) -> (not divides1(2, a))))

axiom odd_divides3 : (forall a:int. ((not divides1(2, a)) -> odd1(a)))

predicate prime1(p: int) = ((2 <= p) and (forall n:int. (((1 < n) and (n < p)) -> (not divides1(n, p)))))

axiom not_prime_11 : (not prime1(1))

axiom prime_21 : prime1(2)

axiom prime_31 : prime1(3)

axiom prime_divisors1 : (forall p:int. (prime1(p) -> (forall d:int. (divides1(d, p) -> ((d = 1) or ((d = (-1)) or ((d = p) or (d = (-p)))))))))

axiom small_divisors1 : (forall p:int. ((2 <= p) -> ((forall d:int. ((2 <= d) -> (prime1(d) -> (((1 < (d * d)) and ((d * d) <= p)) -> (not divides1(d, p)))))) -> prime1(p))))

axiom even_prime1 : (forall p:int. (prime1(p) -> (even1(p) -> (p = 2))))

axiom odd_prime1 : (forall p:int. (prime1(p) -> ((3 <= p) -> odd1(p))))

logic ac gcd1 : int, int -> int

axiom gcd_nonneg1 : (forall a:int. forall b:int. (0 <= gcd1(a, b)))

axiom gcd_def11 : (forall a:int. forall b:int. divides1(gcd1(a, b), a))

axiom gcd_def21 : (forall a:int. forall b:int. divides1(gcd1(a, b), b))

axiom gcd_def31 : (forall a:int. forall b:int. forall x:int. (divides1(x, a) -> (divides1(x, b) -> divides1(x, gcd1(a, b)))))

axiom gcd_unique1 : (forall a:int. forall b:int. forall d:int. ((0 <= d) -> (divides1(d, a) -> (divides1(d, b) -> ((forall x:int. (divides1(x, a) -> (divides1(x, b) -> divides1(x, d)))) -> (d = gcd1(a, b)))))))

axiom gcd_0_pos1 : (forall a:int. ((0 <= a) -> (gcd1(a, 0) = a)))

axiom gcd_0_neg1 : (forall a:int. ((a < 0) -> (gcd1(a, 0) = (-a))))

axiom gcd_opp1 : (forall a:int. forall b:int. (gcd1(a, b) = gcd1((-a), b)))

axiom gcd_euclid1 : (forall a:int. forall b:int. forall q:int. (gcd1(a, b) = gcd1(a, (b - (q * a)))))

axiom Gcd_computer_mod1 : (forall a:int. forall b:int [gcd1(b, safe_comp_mod(a,b))]. ((not (b = 0)) -> (gcd1(b, safe_comp_mod(a,b)) = gcd1(a, b))))

axiom Gcd_euclidean_mod1 : (forall a:int. forall b:int [gcd1(b, safe_eucl_mod(a,b))]. ((not (b = 0)) -> (gcd1(b, safe_eucl_mod(a,b)) = gcd1(a, b))))

axiom gcd_mult1 : (forall a:int. forall b:int. forall c:int. ((0 <= c) -> (gcd1((c * a), (c * b)) = (c * gcd1(a, b)))))

predicate coprime1(a: int, b: int) = (gcd1(a, b) = 1)

axiom prime_coprime3 : (forall p:int. (prime1(p) -> (2 <= p)))

axiom prime_coprime4 : (forall p:int. (prime1(p) -> (forall n:int. (((1 <= n) and (n < p)) -> coprime1(n, p)))))

axiom prime_coprime5 : (forall p:int. (((2 <= p) and (forall n:int. (((1 <= n) and (n < p)) -> coprime1(n, p)))) -> prime1(p)))

axiom Gauss1 : (forall a:int. forall b:int. forall c:int. ((divides1(a, (b * c)) and coprime1(a, b)) -> divides1(a, c)))

axiom Euclid1 : (forall p:int. forall a:int. forall b:int. ((prime1(p) and divides1(p, (a * b))) -> (divides1(p, a) or divides1(p, b))))

type 'a ref1 = { contents1 : 'a }

type 'a list1

logic Nil1 : 'a list1

logic Cons1 : 'a, 'a list1 -> 'a list1

logic match_list1 : 'a list1, 'a1, 'a1 -> 'a1

axiom match_list_Nil1 : (forall z:'a. forall z1:'a. (match_list1((Nil1 : 'a1 list1), z, z1) = z))

axiom match_list_Cons1 : (forall z:'a. forall z1:'a. forall u:'a1. forall u1:'a1 list1. (match_list1(Cons1(u, u1), z, z1) = z1))

logic index_list1 : 'a list1 -> int

axiom index_list_Nil1 : (index_list1((Nil1 : 'a list1)) = 0)

axiom index_list_Cons1 : (forall u:'a. forall u1:'a list1 [Cons1(u, u1)]. (index_list1(Cons1(u, u1)) = 1))

logic Cons_proj_11 : 'a list1 -> 'a

axiom Cons_proj_1_def1 : (forall u:'a. forall u1:'a list1. (Cons_proj_11(Cons1(u, u1)) = u))

logic Cons_proj_21 : 'a list1 -> 'a list1

axiom Cons_proj_2_def1 : (forall u:'a. forall u1:'a list1. (Cons_proj_21(Cons1(u, u1)) = u1))

axiom list_inversion1 : (forall u:'a list1. ((u = (Nil1 : 'a list1)) or (u = Cons1(Cons_proj_11(u), Cons_proj_21(u)))))

goal WP_parameter_largest_prime_factor1 : (forall n:int. ((2 <= n) -> (((2 <= n) and (((2 <= 2) and (2 <= n)) and (forall i:int. (((2 <= i) and (i < 2)) -> (not divides1(i, n)))))) -> (forall d:int. ((((2 <= d) and (d <= n)) and (divides1(d, n) and (forall i:int. (((2 <= i) and (i < d)) -> (not divides1(i, n)))))) -> (forall factors:int list1. ((factors = Cons1(d, (Nil1 : int list1))) -> ((((safe_comp_div(n,d) * d) = n) and divides1(safe_comp_div(n,d), n)) -> ((forall i:int. ((prime1(i) and (divides1(i, n) and (d < i))) -> (coprime1(d, i) and divides1(i, safe_comp_div(n,d))))) -> prime1(d))))))))))

File 2:

axiom match_bool_True : (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))

axiom match_bool_False : (forall z:'a. forall z1:'a. (match_bool(false, z, z1) = z1))

axiom CompatOrderMult : (forall x:int. forall y:int. forall z:int. ((x <= y) -> ((0 <= z) -> ((x * z) <= (y * z)))))

logic abs : int -> int

axiom abs_def : (forall x:int. ((0 <= x) -> (abs(x) = x)))

axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs(x) = (-x))))

axiom Abs_le : (forall x:int. forall y:int. ((abs(x) <= y) -> ((-y) <= x)))

axiom Abs_le1 : (forall x:int. forall y:int. ((abs(x) <= y) -> (x <= y)))

axiom Abs_le2 : (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) -> (abs(x) <= y)))

axiom Abs_pos : (forall x:int. (0 <= abs(x)))

axiom Div_mod : (forall x:int. forall y:int. ((not (y = 0)) -> (x = ((y * safe_comp_div(x,y)) + safe_comp_mod(x,y)))))

axiom Div_bound : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (0 <= safe_comp_div(x,y))))

axiom Div_bound1 : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (safe_comp_div(x,y) <= x)))

axiom Mod_bound : (forall x:int. forall y:int. ((not (y = 0)) -> ((-abs(y)) < safe_comp_mod(x,y))))

axiom Mod_bound1 : (forall x:int. forall y:int. ((not (y = 0)) -> (safe_comp_mod(x,y) < abs(y))))

axiom Div_sign_pos : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (0 <= safe_comp_div(x,y))))

axiom Div_sign_neg : (forall x:int. forall y:int. (((x <= 0) and (0 < y)) -> (safe_comp_div(x,y) <= 0)))

axiom Mod_sign_pos : (forall x:int. forall y:int. (((0 <= x) and (not (y = 0))) -> (0 <= safe_comp_mod(x,y))))

axiom Mod_sign_neg : (forall x:int. forall y:int. (((x <= 0) and (not (y = 0))) -> (safe_comp_mod(x,y) <= 0)))

axiom Rounds_toward_zero : (forall x:int. forall y:int. ((not (y = 0)) -> (abs((safe_comp_div(x,y) * y)) <= abs(x))))

axiom Div_1 : (forall x:int. (safe_comp_div(x,1) = x))

axiom Mod_1 : (forall x:int. (safe_comp_mod(x,1) = 0))

axiom Div_inf : (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> (safe_comp_div(x,y) = 0)))

axiom Mod_inf : (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> (safe_comp_mod(x,y) = x)))

axiom Div_mult : (forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)]. (((0 < x) and ((0 <= y) and (0 <= z))) -> (safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x)))))

axiom Mod_mult : (forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)]. (((0 < x) and ((0 <= y) and (0 <= z))) -> (safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x))))

predicate divides(d: int, n: int) = (exists q:int. (n = (q * d)))

axiom divides_refl : (forall n:int. divides(n, n))

axiom divides_1_n : (forall n:int. divides(1, n))

axiom divides_0 : (forall n:int. divides(n, 0))

axiom divides_left : (forall a:int. forall b:int. forall c:int. (divides(a, b) -> divides((c * a), (c * b))))

axiom divides_right : (forall a:int. forall b:int. forall c:int. (divides(a, b) -> divides((a * c), (b * c))))

axiom divides_oppr : (forall a:int. forall b:int. (divides(a, b) -> divides(a, (-b))))

axiom divides_oppl : (forall a:int. forall b:int. (divides(a, b) -> divides((-a), b)))

axiom divides_oppr_rev : (forall a:int. forall b:int. (divides((-a), b) -> divides(a, b)))

axiom divides_oppl_rev : (forall a:int. forall b:int. (divides(a, (-b)) -> divides(a, b)))

axiom divides_plusr : (forall a:int. forall b:int. forall c:int. (divides(a, b) -> (divides(a, c) -> divides(a, (b + c)))))

axiom divides_minusr : (forall a:int. forall b:int. forall c:int. (divides(a, b) -> (divides(a, c) -> divides(a, (b - c)))))

axiom divides_multl : (forall a:int. forall b:int. forall c:int. (divides(a, b) -> divides(a, (c * b))))

axiom divides_multr : (forall a:int. forall b:int. forall c:int. (divides(a, b) -> divides(a, (b * c))))

axiom divides_factorl : (forall a:int. forall b:int. divides(a, (b * a)))

axiom divides_factorr : (forall a:int. forall b:int. divides(a, (a * b)))

axiom divides_n_1 : (forall n:int. (divides(n, 1) -> ((n = 1) or (n = (-1)))))

axiom divides_antisym : (forall a:int. forall b:int. (divides(a, b) -> (divides(b, a) -> ((a = b) or (a = (-b))))))

axiom divides_trans : (forall a:int. forall b:int. forall c:int. (divides(a, b) -> (divides(b, c) -> divides(a, c))))

axiom divides_bounds : (forall a:int. forall b:int. (divides(a, b) -> ((not (b = 0)) -> (abs(a) <= abs(b)))))

axiom Div_mod1 : (forall x:int. forall y:int. ((not (y = 0)) -> (x = ((y * safe_eucl_div(x,y)) + safe_eucl_mod(x,y)))))

axiom Div_bound2 : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (0 <= safe_eucl_div(x,y))))

axiom Div_bound3 : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (safe_eucl_div(x,y) <= x)))

axiom Mod_bound2 : (forall x:int. forall y:int. ((not (y = 0)) -> (0 <= safe_eucl_mod(x,y))))

axiom Mod_bound3 : (forall x:int. forall y:int. ((not (y = 0)) -> (safe_eucl_mod(x,y) < abs(y))))

axiom Mod_11 : (forall x:int. (safe_eucl_mod(x,1) = 0))

axiom Div_11 : (forall x:int. (safe_eucl_div(x,1) = x))

axiom Div_inf1 : (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> (safe_eucl_div(x,y) = 0)))

axiom Div_inf_neg : (forall x:int. forall y:int. (((0 < x) and (x <= y)) -> (safe_eucl_div((-x),y) = (-1))))

axiom Mod_0 : (forall y:int. ((not (y = 0)) -> (safe_eucl_mod(0,y) = 0)))

axiom Div_1_left : (forall y:int. ((1 < y) -> (safe_eucl_div(1,y) = 0)))

axiom Div_minus1_left : (forall y:int. ((1 < y) -> (safe_eucl_div((-1),y) = (-1))))

axiom Mod_1_left : (forall y:int. ((1 < y) -> (safe_eucl_mod(1,y) = 1)))

axiom Mod_minus1_left : (forall y:int. ((1 < y) -> (safe_eucl_mod((-1),y) = (y - 1))))

axiom Div_mult1 : (forall x:int. forall y:int. forall z:int [safe_eucl_div(((x * y) + z),x)]. ((0 < x) -> (safe_eucl_div(((x * y) + z),x) = (y + safe_eucl_div(z,x)))))

axiom Mod_mult1 : (forall x:int. forall y:int. forall z:int [safe_eucl_mod(((x * y) + z),x)]. ((0 < x) -> (safe_eucl_mod(((x * y) + z),x) = safe_eucl_mod(z,x))))

axiom mod_divides_euclidean : (forall a:int. forall b:int. ((not (b = 0)) -> ((safe_eucl_mod(a,b) = 0) -> divides(b, a))))

axiom divides_mod_euclidean : (forall a:int. forall b:int. ((not (b = 0)) -> (divides(b, a) -> (safe_eucl_mod(a,b) = 0))))

axiom mod_divides_computer : (forall a:int. forall b:int. ((not (b = 0)) -> ((safe_comp_mod(a,b) = 0) -> divides(b, a))))

axiom divides_mod_computer : (forall a:int. forall b:int. ((not (b = 0)) -> (divides(b, a) -> (safe_comp_mod(a,b) = 0))))

predicate even(n: int) = (exists k:int. (n = (2 * k)))

predicate odd(n: int) = (exists k:int. (n = ((2 * k) + 1)))

axiom even_or_odd : (forall n:int. (even(n) or odd(n)))

axiom even_not_odd : (forall n:int. (even(n) -> (not odd(n))))

axiom odd_not_even : (forall n:int. (odd(n) -> (not even(n))))

axiom even_odd : (forall n:int. (even(n) -> odd((n + 1))))

axiom odd_even : (forall n:int. (odd(n) -> even((n + 1))))

axiom even_even : (forall n:int. (even(n) -> even((n + 2))))

axiom odd_odd : (forall n:int. (odd(n) -> odd((n + 2))))

axiom even_2k : (forall k:int. even((2 * k)))

axiom odd_2k1 : (forall k:int. odd(((2 * k) + 1)))

axiom even_divides : (forall a:int. (even(a) -> divides(2, a)))

axiom even_divides1 : (forall a:int. (divides(2, a) -> even(a)))

axiom odd_divides : (forall a:int. (odd(a) -> (not divides(2, a))))

axiom odd_divides1 : (forall a:int. ((not divides(2, a)) -> odd(a)))

predicate prime(p: int) = ((2 <= p) and (forall n:int. (((1 < n) and (n < p)) -> (not divides(n, p)))))

axiom not_prime_1 : (not prime(1))

axiom prime_2 : prime(2)

axiom prime_3 : prime(3)

axiom prime_divisors : (forall p:int. (prime(p) -> (forall d:int. (divides(d, p) -> ((d = 1) or ((d = (-1)) or ((d = p) or (d = (-p)))))))))

axiom small_divisors : (forall p:int. ((2 <= p) -> ((forall d:int. ((2 <= d) -> (prime(d) -> (((1 < (d * d)) and ((d * d) <= p)) -> (not divides(d, p)))))) -> prime(p))))

axiom even_prime : (forall p:int. (prime(p) -> (even(p) -> (p = 2))))

axiom odd_prime : (forall p:int. (prime(p) -> ((3 <= p) -> odd(p))))

logic ac gcd : int, int -> int

axiom gcd_nonneg : (forall a:int. forall b:int. (0 <= gcd(a, b)))

axiom gcd_def1 : (forall a:int. forall b:int. divides(gcd(a, b), a))

axiom gcd_def2 : (forall a:int. forall b:int. divides(gcd(a, b), b))

axiom gcd_def3 : (forall a:int. forall b:int. forall x:int. (divides(x, a) -> (divides(x, b) -> divides(x, gcd(a, b)))))

axiom gcd_unique : (forall a:int. forall b:int. forall d:int. ((0 <= d) -> (divides(d, a) -> (divides(d, b) -> ((forall x:int. (divides(x, a) -> (divides(x, b) -> divides(x, d)))) -> (d = gcd(a, b)))))))

axiom gcd_0_pos : (forall a:int. ((0 <= a) -> (gcd(a, 0) = a)))

axiom gcd_0_neg : (forall a:int. ((a < 0) -> (gcd(a, 0) = (-a))))

axiom gcd_opp : (forall a:int. forall b:int. (gcd(a, b) = gcd((-a), b)))

axiom gcd_euclid : (forall a:int. forall b:int. forall q:int. (gcd(a, b) = gcd(a, (b - (q * a)))))

axiom Gcd_computer_mod : (forall a:int. forall b:int [gcd(b, safe_comp_mod(a,b))]. ((not (b = 0)) -> (gcd(b, safe_comp_mod(a,b)) = gcd(a, b))))

axiom Gcd_euclidean_mod : (forall a:int. forall b:int [gcd(b, safe_eucl_mod(a,b))]. ((not (b = 0)) -> (gcd(b, safe_eucl_mod(a,b)) = gcd(a, b))))

axiom gcd_mult : (forall a:int. forall b:int. forall c:int. ((0 <= c) -> (gcd((c * a), (c * b)) = (c * gcd(a, b)))))

predicate coprime(a: int, b: int) = (gcd(a, b) = 1)

axiom prime_coprime : (forall p:int. (prime(p) -> (2 <= p)))

axiom prime_coprime1 : (forall p:int. (prime(p) -> (forall n:int. (((1 <= n) and (n < p)) -> coprime(n, p)))))

axiom prime_coprime2 : (forall p:int. (((2 <= p) and (forall n:int. (((1 <= n) and (n < p)) -> coprime(n, p)))) -> prime(p)))

axiom Gauss : (forall a:int. forall b:int. forall c:int. ((divides(a, (b * c)) and coprime(a, b)) -> divides(a, c)))

axiom Euclid : (forall p:int. forall a:int. forall b:int. ((prime(p) and divides(p, (a * b))) -> (divides(p, a) or divides(p, b))))

type 'a ref = { contents : 'a }

type 'a list

logic Nil : 'a list

logic Cons : 'a, 'a list -> 'a list

logic match_list : 'a list, 'a1, 'a1 -> 'a1

axiom match_list_Nil : (forall z:'a. forall z1:'a. (match_list((Nil : 'a1 list), z, z1) = z))

axiom match_list_Cons : (forall z:'a. forall z1:'a. forall u:'a1. forall u1:'a1 list. (match_list(Cons(u, u1), z, z1) = z1))

logic index_list : 'a list -> int

axiom index_list_Nil : (index_list((Nil : 'a list)) = 0)

axiom index_list_Cons : (forall u:'a. forall u1:'a list [Cons(u, u1)]. (index_list(Cons(u, u1)) = 1))

logic Cons_proj_1 : 'a list -> 'a

axiom Cons_proj_1_def : (forall u:'a. forall u1:'a list. (Cons_proj_1(Cons(u, u1)) = u))

logic Cons_proj_2 : 'a list -> 'a list

axiom Cons_proj_2_def : (forall u:'a. forall u1:'a list. (Cons_proj_2(Cons(u, u1)) = u1))

axiom list_inversion : (forall u:'a list. ((u = (Nil : 'a list)) or (u = Cons(Cons_proj_1(u), Cons_proj_2(u)))))

goal WP_parameter_largest_prime_factor : (forall n:int. ((2 <= n) -> (((2 <= n) and (((2 <= 2) and (2 <= n)) and (forall i:int. (((2 <= i) and (i < 2)) -> (not divides(i, n)))))) -> (forall d:int. ((((2 <= d) and (d <= n)) and (divides(d, n) and (forall i:int. (((2 <= i) and (i < d)) -> (not divides(i, n)))))) -> (forall factors:int list. ((factors = Cons(d, (Nil : int list))) -> ((((safe_comp_div(n,d) * d) = n) and divides(safe_comp_div(n,d), n)) -> ((forall i:int. ((prime(i) and (divides(i, n) and (d < i))) -> (coprime(d, i) and divides(i, safe_comp_div(n,d))))) -> (forall target:int. forall factor:int. forall factors1:int list. ((((1 <= target) and (target <= n)) and (((2 <= factor) and (factor <= n)) and (divides(factor, n) and (prime(factor) and ((forall i:int. ((divides(i, target) and (2 <= i)) -> ((factor <= i) and divides(i, n)))) and (forall i:int. ((prime(i) and (divides(i, n) and (factor < i))) -> divides(i, target)))))))) -> ((2 <= target) -> ((divides(target, target) and ((2 <= target) and (factor <= target))) -> (((2 <= target) and (((2 <= factor) and (factor <= target)) and (forall i:int. (((2 <= i) and (i < factor)) -> (not divides(i, target)))))) -> (forall d1:int. ((((factor <= d1) and (d1 <= target)) and (divides(d1, target) and (forall i:int. (((2 <= i) and (i < d1)) -> (not divides(i, target)))))) -> (prime(d1) -> (forall factor1:int. ((factor1 = d1) -> (forall factors2:int list. ((factors2 = Cons(d1, factors1)) -> (forall target1:int. ((target1 = safe_comp_div(target,d1)) -> ((((target1 * d1) = target) and divides(target1, target)) -> ((forall i:int. ((prime(i) and (divides(i, n) and (d1 < i))) -> ((factor < i) and (divides(i, target) and (((1 <= d1) and (d1 < i)) and (coprime(d1, i) and divides(i, target1))))))) -> (forall i:int. ((divides(i, target1) and (2 <= i)) -> ((factor1 <= i) and divides(i, n)))))))))))))))))))))))))))))

OCamlPro / alt-ergo

alt-ergo crash #1