From 654254ca2e6ac94d3e0c62a127f92caff4b5938c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 29 Jul 2019 21:24:11 +0200
Subject: Use the precondition of diveucl_21 to avoid massaging the dividend.

All the implementations now return (0, 0) when the dividend is so large
that the quotient would overflow.
---
 test-suite/arithmetic/diveucl_21.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite/arithmetic')

diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/arithmetic/diveucl_21.v
index bd76df12ce..b12dba429c 100644
--- a/test-suite/arithmetic/diveucl_21.v
+++ b/test-suite/arithmetic/diveucl_21.v
@@ -10,11 +10,11 @@ Check (eq_refl (4611686018427387904,1) <<: diveucl_21 1 1 2 = (46116860184273879
 Definition compute1 := Eval compute in diveucl_21 1 1 2.
 Check (eq_refl compute1 : (4611686018427387904,1) = (4611686018427387904,1)).
 
-Check (eq_refl : diveucl_21 3 1 2 = (4611686018427387904, 1)).
-Check (eq_refl (4611686018427387904, 1) <: diveucl_21 3 1 2 = (4611686018427387904, 1)).
-Check (eq_refl (4611686018427387904, 1) <<: diveucl_21 3 1 2 = (4611686018427387904, 1)).
+Check (eq_refl : diveucl_21 3 1 2 = (0, 0)).
+Check (eq_refl (0, 0) <: diveucl_21 3 1 2 = (0, 0)).
+Check (eq_refl (0, 0) <<: diveucl_21 3 1 2 = (0, 0)).
 Definition compute2 := Eval compute in diveucl_21 3 1 2.
-Check (eq_refl compute2 : (4611686018427387904, 1) = (4611686018427387904, 1)).
+Check (eq_refl compute2 : (0, 0) = (0, 0)).
 
 Check (eq_refl : diveucl_21 1 1 0 = (0,0)).
 Check (eq_refl (0,0) <: diveucl_21 1 1 0 = (0,0)).
-- 
cgit v1.2.3