Commit eedb7053 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

add a test for the bug 20445 that resurected

parent 9c9b6394
module A
axiom G : true
end
module B
goal G : false
clone A with goal G
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../20445.mlw">
<theory name="A" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="B" sum="3e4e0db7222351ee8b39dde6ac341e91">
<goal name="G">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
<proof prover="1" timelimit="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="unknown" time="0.02"/></proof>
<proof prover="3"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="G" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
</file>
</why3session>
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