[Ada] Fix automatic proof on System.Arith_32

gcc/ada/

	* libgnat/s-arit32.adb (Scaled_Divide32): Add an assertion, move
	the call of Prove_Sign_R around.

diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb
index 6dac5725a59e4bca7948c3d33bb40138d9b53756..c3d9f6a50bc3c68c5cd775aeca014e8ceccdf77f 100644 (file)
--- a/gcc/ada/libgnat/s-arit32.adb
+++ b/gcc/ada/libgnat/s-arit32.adb
@@ -541,8 +541,10 @@ is
          end if;
       end if;
 
+      pragma Assert (In_Int32_Range (Big_Q));
       pragma Assert (Big (Qu) = abs Big_Q);
       pragma Assert (Big (Ru) = abs Big_R);
+      Prove_Sign_R;
 
       --  Set final signs (RM 4.5.5(27-30))
 
@@ -563,7 +565,6 @@ is
          Q := (if Z > 0 then To_Neg_Int (Qu) else To_Pos_Int (Qu));
       end if;
 
-      Prove_Sign_R;
       Prove_Signs;
    end Scaled_Divide32;