Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt code to SPARK FSF and rewrite parsing algorithm for ATBB #127

Merged
merged 10 commits into from
Jul 19, 2024
Merged

Adapt code to SPARK FSF and rewrite parsing algorithm for ATBB #127

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
1f6aacd
Add SPARKlib project file
joffreyhuguet May 6, 2024
67f6de1
Adapt code to new SPARK
joffreyhuguet May 7, 2024
867ed69
Replace Error mechansism in ATBB string parsing with exceptional cases
joffreyhuguet May 31, 2024
53bc726
Maintain proofs with newer SPARK
joffreyhuguet May 31, 2024
dc5df03
Prove termination of SPARK services
joffreyhuguet May 31, 2024
bea2a9f
Update session files and fix one issue in code
joffreyhuguet May 31, 2024
84546d4
Update session files and test outputs
joffreyhuguet Jun 5, 2024
5c9d755
Update proof test script to generate a sparklib.gpr
joffreyhuguet Jun 5, 2024
bd5d463
Modify Int64 parsing algorithm and update session files
joffreyhuguet Jul 16, 2024
b1084c5
Support GNATprove FSF 14
manthonyaiello Jul 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
The diff you're trying to view is too large. We only load the first 3000 changed files.
4 changes: 2 additions & 2 deletions infrastructure/install-libexec/install-gnat.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@
ALR_SETTINGS_DIR,
"toolchain",
"--select",
"gnat_native^13",
"gnat_native^14",
"gprbuild^22",
],
description="Install GNAT toolchain using alr",
Expand All @@ -105,7 +105,7 @@
"-s",
ALR_SETTINGS_DIR,
"get",
"gnatprove^13",
"gnatprove^14",
],
description="Install GNATprove using alr",
cwd=ALR_DIR,
Expand Down
26 changes: 16 additions & 10 deletions ...ada/proof/sessions/0074b76feb6e1a897482-del__hash_checks__hash_equivalent/why3session.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,31 +2,37 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="CVC5" version="0.0.7-gnatprove" timelimit="0" steplimit="3791" memlimit="0"/>
<prover id="1" name="Trivial" version="1.0" alternative="trivial" timelimit="1" steplimit="1" memlimit="1000"/>
<prover id="0" name="altergo" version="1.30-gnatprove" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC5" version="0.0.7-gnatprove" timelimit="0" steplimit="1055" memlimit="0"/>
<prover id="2" name="Z3" version="4.5.1-gnatprove" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Trivial" version="1.0" alternative="trivial" timelimit="1" steplimit="1" memlimit="1000"/>
<file format="gnat-json" proved="true">
<path name=".."/><path name=".."/><path name=".."/><path name="objs"/>
<path name="release"/><path name="gnatprove"/><path name="0074b76feb6e1a897482-del__hash_checks__hash_equivalent.gnat-json"/>
<path name=".."/><path name=".."/><path name=".."/><path name=".."/><path name=".."/>
<path name=".."/><path name=".."/><path name=".."/><path name=".."/><path name=".."/>
<path name="tmp"/><path name="tmpux6py1be"/><path name="route_aggregator"/>
<path name="gnatprove"/><path name="0074b76feb6e1a897482-del__hash_checks__hash_equivalent.gnat-json"/>
<theory name="Route_aggregator__int64_idplanpair_maps__formal_model__hash_checks__hash_equivalent__subprogram_def" proved="true">
<goal name="def&#39;vc" proved="true">
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="valid" steps="3446"/></proof>
<proof prover="0" obsolete="true"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="959"/></proof>
<proof prover="2" obsolete="true"><result status="valid" steps="498"/></proof>
</goal>
</transf>
</goal>
Expand Down
17 changes: 17 additions & 0 deletions src/ada/proof/sessions/0074b76feb6e1a897482-del__hash_checks__hash_equivalent/why3shapes
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
(* shapes version: 6 *)
tLiaFalseaTruea=V1V0LiaFalseaTruea=V1V0LaxLayIadynamic_invariantayaTrueaFalseaTrueaTrueIadynamic_invariantaxaTrueaFalseaTrueaTrue
empty_shape
tIa=axayIadynamic_invariantayaTrueaFalseaTrueaTrueIadynamic_invariantaxaTrueaFalseaTrueaTrue
tLayItAtAtIa=axayIadynamic_invariantayaTrueaFalseaTrueaTrueIadynamic_invariantaxaTrueaFalseaTrueaTrue
tLaxLV1Ia=V1aof_intamodV0a_two_power_sizeAadynamic_invariantV1aTrueaFalseaTrueaTrueAaint64_hash__function_guardV1V0Laint64_hashV0LayItAtAtIa=axayIadynamic_invariant1ayaTrueaFalseaTrueaTrueIadynamic_invariant1axaTrueaFalseaTrueaTrue
tLiaFalseaTruea=V4V1LiaFalseaTruea=V4V1LV4Ia=V4aof_intamodV3a_two_power_sizeAadynamic_invariantV4aTrueaFalseaTrueaTrueAaint64_hash__function_guardV4V3Laint64_hashV3LaxLV1Ia=V1aof_intamodV0a_two_power_sizeAadynamic_invariantV1aTrueaFalseaTrueaTrueAaint64_hash__function_guardV1V0Laint64_hashV0LayItAtAtIa=axayIadynamic_invariant1ayaTrueaFalseaTrueaTrueIadynamic_invariant1axaTrueaFalseaTrueaTrue
a=eaint64_hash__function_guardV0axAa=V0aint64_hashaxeaint64_hash__function_guardV1ayAa=V1aint64_hashayItAtAtIa=axayIadynamic_invariantayaTrueaFalseaTrueaTrueIadynamic_invariantaxaTrueaFalseaTrueaTrue
a=eaint64_hash__function_guardV0axAa=V0aint64_hashaxeaint64_hash__function_guardV1ayAa=V1aint64_hashayAtLiaFalseaTruea=V6V3LiaFalseaTruea=V6V3LV6Ia=V6aof_intamodV5a_two_power_sizeAadynamic_invariantV6aTrueaFalseaTrueaTrueAaint64_hash__function_guardV6V5Laint64_hashV5AtLaxLV3Ia=V3aof_intamodV2a_two_power_sizeAadynamic_invariantV3aTrueaFalseaTrueaTrueAaint64_hash__function_guardV3V2Laint64_hashV2AtLayItAtAtAtIa=axayAtLiaFalseaTruea=V11V10LiaFalseaTruea=V11V10LaxLayIadynamic_invariant1ayaTrueaFalseaTrueaTrueIadynamic_invariant1axaTrueaFalseaTrueaTrue

5fa3fdd6d6385d63c4962118228ced8e 1H7
9638152f3f80e460c8d9f701a0784536 1H0
607e465521067bac695bb2014b6acacf 1H2
828577a421b60271d2d5293f96666aa1 1H3
ac41e9008bd0537164cc11db6e908418 1H4
45701db76b50eb77fb0d6b0994acf583 1H5
f35abd96a0153454020bd351fe8bf609 1H6
17 changes: 17 additions & 0 deletions src/ada/proof/sessions/0074b76feb6e1a897482-del__hash_checks__hash_equivalent/why3shapes.bak
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
(* shapes version: 6 *)
tLiaFalseaTruea=V1V0LiaFalseaTruea=V1V0LaxLayIadynamic_invariantayaTrueaFalseaTrueaTrueIadynamic_invariantaxaTrueaFalseaTrueaTrue
empty_shape
tIa=axayIadynamic_invariantayaTrueaFalseaTrueaTrueIadynamic_invariantaxaTrueaFalseaTrueaTrue
tLayItAtAtIa=axayIadynamic_invariantayaTrueaFalseaTrueaTrueIadynamic_invariantaxaTrueaFalseaTrueaTrue
tLaxLV1Ia=V1aof_intamodV0a_two_power_sizeAadynamic_invariantV1aTrueaFalseaTrueaTrueAaint64_hash__function_guardV1V0Laint64_hashV0LayItAtAtIa=axayIadynamic_invariant1ayaTrueaFalseaTrueaTrueIadynamic_invariant1axaTrueaFalseaTrueaTrue
tLiaFalseaTruea=V4V1LiaFalseaTruea=V4V1LV4Ia=V4aof_intamodV3a_two_power_sizeAadynamic_invariantV4aTrueaFalseaTrueaTrueAaint64_hash__function_guardV4V3Laint64_hashV3LaxLV1Ia=V1aof_intamodV0a_two_power_sizeAadynamic_invariantV1aTrueaFalseaTrueaTrueAaint64_hash__function_guardV1V0Laint64_hashV0LayItAtAtIa=axayIadynamic_invariant1ayaTrueaFalseaTrueaTrueIadynamic_invariant1axaTrueaFalseaTrueaTrue
a=eaint64_hash__function_guardV0axAa=V0aint64_hashaxeaint64_hash__function_guardV1ayAa=V1aint64_hashayItAtAtIa=axayIadynamic_invariantayaTrueaFalseaTrueaTrueIadynamic_invariantaxaTrueaFalseaTrueaTrue
a=eaint64_hash__function_guardV0axAa=V0aint64_hashaxeaint64_hash__function_guardV1ayAa=V1aint64_hashayAtLiaFalseaTruea=V6V3LiaFalseaTruea=V6V3LV6Ia=V6aof_intamodV5a_two_power_sizeAadynamic_invariantV6aTrueaFalseaTrueaTrueAaint64_hash__function_guardV6V5Laint64_hashV5AtLaxLV3Ia=V3aof_intamodV2a_two_power_sizeAadynamic_invariantV3aTrueaFalseaTrueaTrueAaint64_hash__function_guardV3V2Laint64_hashV2AtLayItAtAtAtIa=axayAtLiaFalseaTruea=V11V10LiaFalseaTruea=V11V10LaxLayIadynamic_invariant1ayaTrueaFalseaTrueaTrueIadynamic_invariant1axaTrueaFalseaTrueaTrue

5fa3fdd6d6385d63c4962118228ced8e 1H7
9638152f3f80e460c8d9f701a0784536 1H0
607e465521067bac695bb2014b6acacf 1H2
828577a421b60271d2d5293f96666aa1 1H3
ac41e9008bd0537164cc11db6e908418 1H4
45701db76b50eb77fb0d6b0994acf583 1H5
f35abd96a0153454020bd351fe8bf609 1H6
262 changes: 262 additions & 0 deletions ...ada/proof/sessions/009045c7cd84894ed48c-31__action_in_taskplanoptions_map/why3session.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,262 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="CVC5" version="0.0.7-gnatprove" timelimit="0" steplimit="6645" memlimit="0"/>
<prover id="1" name="Trivial" version="1.0" alternative="trivial" timelimit="1" steplimit="1" memlimit="1000"/>
<file format="gnat-json" proved="true">
<path name=".."/><path name=".."/><path name=".."/><path name=".."/><path name=".."/>
<path name=".."/><path name=".."/><path name=".."/><path name=".."/><path name=".."/>
<path name="tmp"/><path name="tmpux6py1be"/><path name="assignment_tree_branch_bound"/>
<path name="gnatprove"/><path name="009045c7cd84894ed48c-31__action_in_taskplanoptions_map.gnat-json"/>
<theory name="Assignment_tree_branch_bound__initialize_algebra__B_31__action_in_taskplanoptions_map__subprogram_def" proved="true">
<goal name="def&#39;vc" proved="true">
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0" steplimit="3813"><result status="valid" steps="3466"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0" steplimit="4471"><result status="valid" steps="4064"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0" steplimit="4467"><result status="valid" steps="4060"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="0" steplimit="5041"><result status="valid" steps="4582"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0" steplimit="5041"><result status="valid" steps="4582"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0" steplimit="33732"><result status="valid" steps="30665"/></proof>
</goal>
<goal name="def&#39;vc.13" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
<proof prover="0" steplimit="75651"><result status="valid" steps="68773"/></proof>
</goal>
<goal name="def&#39;vc.15" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.16" proved="true">
<proof prover="0" steplimit="79110"><result status="valid" steps="71918"/></proof>
</goal>
<goal name="def&#39;vc.17" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.18" proved="true">
<proof prover="0" steplimit="79796"><result status="valid" steps="72541"/></proof>
</goal>
<goal name="def&#39;vc.19" proved="true">
<proof prover="0" steplimit="7495"><result status="valid" steps="6813"/></proof>
</goal>
<goal name="def&#39;vc.20" proved="true">
<proof prover="0" steplimit="35157"><result status="valid" steps="31960"/></proof>
</goal>
<goal name="def&#39;vc.21" proved="true">
<proof prover="0" steplimit="6223"><result status="valid" steps="5657"/></proof>
</goal>
<goal name="def&#39;vc.22" proved="true">
<proof prover="0" steplimit="6219"><result status="valid" steps="5653"/></proof>
</goal>
<goal name="def&#39;vc.23" proved="true">
<proof prover="0"><result status="valid" steps="6040"/></proof>
</goal>
<goal name="def&#39;vc.24" proved="true">
<proof prover="0"><result status="valid" steps="6040"/></proof>
</goal>
<goal name="def&#39;vc.25" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.26" proved="true">
<proof prover="0" steplimit="37517"><result status="valid" steps="34106"/></proof>
</goal>
<goal name="def&#39;vc.27" proved="true">
<proof prover="0" steplimit="37525"><result status="valid" steps="34113"/></proof>
</goal>
<goal name="def&#39;vc.28" proved="true">
<proof prover="0" steplimit="83174"><result status="valid" steps="75612"/></proof>
</goal>
<goal name="def&#39;vc.29" proved="true">
<proof prover="0" steplimit="9367"><result status="valid" steps="8515"/></proof>
</goal>
<goal name="def&#39;vc.30" proved="true">
<proof prover="0" steplimit="38008"><result status="valid" steps="34552"/></proof>
</goal>
<goal name="def&#39;vc.31" proved="true">
<proof prover="0" steplimit="7770"><result status="valid" steps="7063"/></proof>
</goal>
<goal name="def&#39;vc.32" proved="true">
<proof prover="0" steplimit="7770"><result status="valid" steps="7063"/></proof>
</goal>
<goal name="def&#39;vc.33" proved="true">
<proof prover="0" steplimit="8131"><result status="valid" steps="7391"/></proof>
</goal>
<goal name="def&#39;vc.34" proved="true">
<proof prover="0" steplimit="8131"><result status="valid" steps="7391"/></proof>
</goal>
<goal name="def&#39;vc.35" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.36" proved="true">
<proof prover="0" steplimit="38103"><result status="valid" steps="34639"/></proof>
</goal>
<goal name="def&#39;vc.37" proved="true">
<proof prover="0" steplimit="83773"><result status="valid" steps="76157"/></proof>
</goal>
<goal name="def&#39;vc.38" proved="true">
<proof prover="0" steplimit="38519"><result status="valid" steps="35017"/></proof>
</goal>
<goal name="def&#39;vc.39" proved="true">
<proof prover="0" steplimit="38584"><result status="valid" steps="35076"/></proof>
</goal>
<goal name="def&#39;vc.40" proved="true">
<proof prover="0" steplimit="8284"><result status="valid" steps="7530"/></proof>
</goal>
<goal name="def&#39;vc.41" proved="true">
<proof prover="0" steplimit="8284"><result status="valid" steps="7530"/></proof>
</goal>
<goal name="def&#39;vc.42" proved="true">
<proof prover="0" steplimit="8675"><result status="valid" steps="7886"/></proof>
</goal>
<goal name="def&#39;vc.43" proved="true">
<proof prover="0" steplimit="8675"><result status="valid" steps="7886"/></proof>
</goal>
<goal name="def&#39;vc.44" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.45" proved="true">
<proof prover="0" steplimit="40562"><result status="valid" steps="36874"/></proof>
</goal>
<goal name="def&#39;vc.46" proved="true">
<proof prover="0" steplimit="40592"><result status="valid" steps="36901"/></proof>
</goal>
<goal name="def&#39;vc.47" proved="true">
<proof prover="0" steplimit="87158"><result status="valid" steps="79234"/></proof>
</goal>
<goal name="def&#39;vc.48" proved="true">
<proof prover="0" steplimit="11357"><result status="valid" steps="10324"/></proof>
</goal>
<goal name="def&#39;vc.49" proved="true">
<proof prover="0" steplimit="40784"><result status="valid" steps="37076"/></proof>
</goal>
<goal name="def&#39;vc.50" proved="true">
<proof prover="0" steplimit="9698"><result status="valid" steps="8816"/></proof>
</goal>
<goal name="def&#39;vc.51" proved="true">
<proof prover="0" steplimit="9698"><result status="valid" steps="8816"/></proof>
</goal>
<goal name="def&#39;vc.52" proved="true">
<proof prover="0" steplimit="10123"><result status="valid" steps="9202"/></proof>
</goal>
<goal name="def&#39;vc.53" proved="true">
<proof prover="0" steplimit="10123"><result status="valid" steps="9202"/></proof>
</goal>
<goal name="def&#39;vc.54" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.55" proved="true">
<proof prover="0" steplimit="89719"><result status="valid" steps="81562"/></proof>
</goal>
<goal name="def&#39;vc.56" proved="true">
<proof prover="0" steplimit="80316"><result status="valid" steps="73014"/></proof>
</goal>
<goal name="def&#39;vc.57" proved="true">
<proof prover="0" steplimit="80312"><result status="valid" steps="73010"/></proof>
</goal>
<goal name="def&#39;vc.58" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.59" proved="true">
<proof prover="0" steplimit="80987"><result status="valid" steps="73624"/></proof>
</goal>
<goal name="def&#39;vc.60" proved="true">
<proof prover="0" steplimit="80983"><result status="valid" steps="73620"/></proof>
</goal>
<goal name="def&#39;vc.61" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.62" proved="true">
<proof prover="0" steplimit="7783"><result status="valid" steps="7075"/></proof>
</goal>
<goal name="def&#39;vc.63" proved="true">
<proof prover="0" steplimit="8992"><result status="valid" steps="8174"/></proof>
</goal>
<goal name="def&#39;vc.64" proved="true">
<proof prover="0" steplimit="8992"><result status="valid" steps="8174"/></proof>
</goal>
<goal name="def&#39;vc.65" proved="true">
<proof prover="0" steplimit="9315"><result status="valid" steps="8468"/></proof>
</goal>
<goal name="def&#39;vc.66" proved="true">
<proof prover="0" steplimit="9315"><result status="valid" steps="8468"/></proof>
</goal>
<goal name="def&#39;vc.67" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.68" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.69" proved="true">
<proof prover="0" steplimit="87618"><result status="valid" steps="79652"/></proof>
</goal>
<goal name="def&#39;vc.70" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.71" proved="true">
<proof prover="0" steplimit="12759"><result status="valid" steps="11599"/></proof>
</goal>
<goal name="def&#39;vc.72" proved="true">
<proof prover="0" steplimit="13599"><result status="valid" steps="12362"/></proof>
</goal>
<goal name="def&#39;vc.73" proved="true">
<proof prover="0" steplimit="13599"><result status="valid" steps="12362"/></proof>
</goal>
<goal name="def&#39;vc.74" proved="true">
<proof prover="0" steplimit="13865"><result status="valid" steps="12604"/></proof>
</goal>
<goal name="def&#39;vc.75" proved="true">
<proof prover="0" steplimit="13865"><result status="valid" steps="12604"/></proof>
</goal>
<goal name="def&#39;vc.76" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.77" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.78" proved="true">
<proof prover="1"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.79" proved="true">
<proof prover="0" steplimit="97591"><result status="valid" steps="88719"/></proof>
</goal>
<goal name="def&#39;vc.80" proved="true">
<proof prover="0" steplimit="92992"><result status="valid" steps="84538"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Loading