From: Yannick Moy
The proof of System.Arith_Double still required the use of
CVC4, now replaced by its successor cvc5. Adapt the proof to be
able to remove CVC4 in the proof of run-time units.
gcc/ada/
* libgnat/s-aridou.adb (Lemma_Div_Mult): New simple lemma.
(Lemma_Powers_Of_2
Update to version 4.8.14 of prover Z3 requires minor adjustments of the
ghost code to add necessary intermediate assertions that drive the
automatic proof.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-aridou.adb (Double_Divide, Scaled_Divide): Add
interm
Following changes in GNATprove, ghost code needs some adjustments for
proof to go through.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-aridou.adb (Double_Divide): Adjust proof of lemma
Prove_Signs, call lemma for commutation of Big and
multiplic
