• MARCHE Claude's avatar
    Execution: support for div/mod operators. Test with · ae28438f
    MARCHE Claude authored
    why3 -P alt-ergo examples/tests-provers/div.why -T EuclideanDivTest --eval div_m1_2 --eval mod_m1_2 --eval div_1_m2 --eval mod_1_m2 --eval div_m1_m2 --eval mod_m1_m2
    
    why3 -P alt-ergo examples/tests-provers/div.why -T ComputerDivTest --eval div_m1_2 --eval mod_m1_2 --eval div_1_m2 --eval mod_1_m2 --eval div_m1_m2 --eval mod_m1_m2
    
    why3 examples/euler001.mlw --exec Euler001.run
    ae28438f
div.why 1.31 KB