Commit 922c54fb authored by Sylvain Dailler's avatar Sylvain Dailler

Update test 13 and 14.

Should solve failing bench problem.
parent ae2ebcd9
......@@ -3,7 +3,9 @@ module Test
use import int.Int
axiom a : 15 = 2 + 3 + 6
constant c : int
axiom a : c * 0 + 15 = 2 + 3 + 6
goal g: True
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../13_compute_in.mlw">
<theory name="Test" sum="c291ec30c4881b6eb0ae96cce497dffc">
<theory name="Test" sum="0f62b987219641c9a62fe01b2edf29de">
<goal name="g">
<transf name="compute_hyp" arg1="in" arg2="a">
<goal name="g.0">
......
......@@ -2,9 +2,9 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../14_simpl.mlw" proved="true">
<theory name="Test" proved="true" sum="22cf7419b518c45bfba8210f6a346e58">
<goal name="g10" proved="true">
<file name="../14_simpl.mlw">
<theory name="Test" sum="22cf7419b518c45bfba8210f6a346e58">
<goal name="g10">
<transf name="step" arg1="in" arg2="g10">
<goal name="g10.0">
<transf name="step" arg1="in" arg2="g10">
......@@ -13,28 +13,14 @@
</transf>
</goal>
</transf>
<transf name="step" proved="true" >
<goal name="g10.0" proved="true">
<transf name="step" proved="true" >
</transf>
</goal>
</transf>
</goal>
<goal name="g11" proved="true">
<transf name="step" proved="true" arg1="in" arg2="g11">
<transf name="step" proved="true" >
<goal name="g11.0" proved="true">
<transf name="step" proved="true" arg1="in" arg2="g11">
<goal name="g11.0.0" proved="true">
<transf name="step" proved="true" >
</transf>
</goal>
<transf name="step" proved="true" >
</transf>
</goal>
</transf>
<transf name="step" >
<goal name="g11.0">
</goal>
</transf>
</goal>
</theory>
</file>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment