diff --git a/imp_test/why3session.xml b/imp_test/why3session.xml index a511523a70a729e52898c37d648cc9b66a030e2a..1e004b540f04b60fad22dc0e6dff1d51b737d113 100644 --- a/imp_test/why3session.xml +++ b/imp_test/why3session.xml @@ -2,236 +2,32 @@ <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" "http://why3.lri.fr/why3session.dtd"> <why3session shape_version="5"> -<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> -<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/> -<file name="../state.mlw" proved="true"> -<theory name="State" proved="true"> - <goal name="VC get" expl="VC for get" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> +<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/> +<file name="../imp_test.mlw" proved="true"> +<theory name="Imp_test" proved="true"> + <goal name="ex1" proved="true"> + <proof prover="0"><result status="valid" time="0.02" steps="82"/></proof> </goal> - <goal name="VC set" expl="VC for set" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> + <goal name="ex2" proved="true"> + <proof prover="0"><result status="valid" time="0.03" steps="101"/></proof> </goal> - <goal name="VC mixfix []" expl="VC for mixfix []" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC mixfix [<-]" expl="VC for mixfix [<-]" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC const" expl="VC for const" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof> - </goal> -</theory> -<theory name="Reg" proved="true"> - <goal name="VC read" expl="VC for read" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC write" expl="VC for write" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC const" expl="VC for const" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof> - </goal> -</theory> -</file> -<file name="../imp_test.mlw"> -<theory name="Imp_test"> - <goal name="ex1"> - <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="82"/></proof> - </goal> - <goal name="ex2"> - <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="101"/></proof> - </goal> - <goal name="ex3"> - <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof> - <proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof> + <goal name="ex3" proved="true"> + <proof prover="0"><result status="valid" time="0.03" steps="97"/></proof> </goal> <goal name="ex4" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="97"/></proof> - </goal> - <goal name="ex5"> - <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof> - </goal> - <goal name="ex6"> - <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="74"/></proof> - </goal> - <goal name="ex7"> - <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="84"/></proof> + <proof prover="0"><result status="valid" time="0.03" steps="97"/></proof> </goal> - <goal name="ex8"> - <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="100"/></proof> - </goal> -</theory> -</file> -<file name="../imp_ex.mlw" proved="true"> -<theory name="Imp_Ex" proved="true"> - <goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true"> - <proof prover="0"><result status="valid" time="0.52" steps="783"/></proof> - </goal> - <goal name="VC beval_ex" expl="VC for beval_ex" proved="true"> - <proof prover="0"><result status="valid" time="0.22" steps="667"/></proof> - </goal> - <goal name="VC ceval_ex" expl="VC for ceval_ex" proved="true"> - <proof prover="0"><result status="valid" time="0.08" steps="237"/></proof> - </goal> -</theory> -</file> -<file name="../imp_ex_assignment.mlw"> -<theory name="Imp_ex"> - <goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true"> - <proof prover="0"><result status="valid" time="0.68" steps="783"/></proof> - </goal> - <goal name="VC beval_ex" expl="VC for beval_ex" proved="true"> - <proof prover="0"><result status="valid" time="0.20" steps="667"/></proof> - </goal> - <goal name="VC ceval_ex" expl="VC for ceval_ex"> - <transf name="split_vc" > - <goal name="VC ceval_ex.0" expl="postcondition" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="74"/></proof> - </goal> - <goal name="VC ceval_ex.1" expl="postcondition"> - <proof prover="0"><result status="timeout" time="1.00"/></proof> - </goal> - <goal name="VC ceval_ex.2" expl="postcondition"> - <proof prover="0"><result status="timeout" time="1.00"/></proof> - </goal> - <goal name="VC ceval_ex.3" expl="postcondition"> - <proof prover="0"><result status="timeout" time="1.00"/></proof> - </goal> - <goal name="VC ceval_ex.4" expl="postcondition"> - <proof prover="0"><result status="timeout" time="1.00"/></proof> - </goal> - </transf> - </goal> -</theory> -</file> -<file name="../imp.mlw" proved="true"> -<theory name="Imp" proved="true"> - <goal name="ceval_deterministic_aux" proved="true"> - <transf name="induction_pr" proved="true" > - <goal name="ceval_deterministic_aux.0" proved="true"> - <proof prover="0"><result status="valid" time="0.05" steps="135"/></proof> - </goal> - <goal name="ceval_deterministic_aux.1" proved="true"> - <proof prover="0"><result status="valid" time="0.08" steps="180"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2" proved="true"> - <transf name="induction_pr" proved="true" > - <goal name="ceval_deterministic_aux.2.0" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.1" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.2" proved="true"> - <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof> - <proof prover="1"><result status="valid" time="0.11"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.3" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.4" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.5" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.6" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof> - </goal> - </transf> - </goal> - <goal name="ceval_deterministic_aux.3" proved="true"> - <transf name="induction_pr" proved="true" > - <goal name="ceval_deterministic_aux.3.0" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.1" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.2" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.3" proved="true"> - <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof> - <proof prover="1"><result status="valid" time="0.06"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.4" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.5" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="85"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.6" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof> - </goal> - </transf> - </goal> - <goal name="ceval_deterministic_aux.4" proved="true"> - <transf name="induction_pr" proved="true" > - <goal name="ceval_deterministic_aux.4.0" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.1" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.2" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.3" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.4" proved="true"> - <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof> - <proof prover="1"><result status="valid" time="0.06"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.5" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.6" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof> - </goal> - </transf> - </goal> - <goal name="ceval_deterministic_aux.5" proved="true"> - <proof prover="0"><result status="valid" time="0.05" steps="133"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6" proved="true"> - <transf name="induction_pr" proved="true" > - <goal name="ceval_deterministic_aux.6.0" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.1" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.2" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.3" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.4" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.5" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.6" proved="true"> - <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof> - <proof prover="1"><result status="valid" time="0.11"/></proof> - </goal> - </transf> - </goal> - </transf> + <goal name="ex5" proved="true"> + <proof prover="0"><result status="valid" time="0.04" steps="97"/></proof> </goal> - <goal name="ceval_deterministic" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="107"/></proof> + <goal name="ex6" proved="true"> + <proof prover="0"><result status="valid" time="0.02" steps="74"/></proof> </goal> - <goal name="VC beval"> - <proof prover="0"><result status="valid" time="0.02" steps="73"/></proof> + <goal name="ex7" proved="true"> + <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof> </goal> - <goal name="VC aeval"> - <proof prover="0"><result status="valid" time="0.01" steps="73"/></proof> + <goal name="ex8" proved="true"> + <proof prover="0"><result status="valid" time="0.03" steps="100"/></proof> </goal> </theory> </file> diff --git a/imp_test/why3session.xml.bak b/imp_test/why3session.xml.bak deleted file mode 100644 index 428557c944439ba953d1200d5dc192a91bd6887f..0000000000000000000000000000000000000000 --- a/imp_test/why3session.xml.bak +++ /dev/null @@ -1,238 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" -"http://why3.lri.fr/why3session.dtd"> -<why3session shape_version="5"> -<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> -<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/> -<file name="../state.mlw" proved="true"> -<theory name="State" proved="true"> - <goal name="VC get" expl="VC for get" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC set" expl="VC for set" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC mixfix []" expl="VC for mixfix []" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC mixfix [<-]" expl="VC for mixfix [<-]" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC const" expl="VC for const" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof> - </goal> -</theory> -<theory name="Reg" proved="true"> - <goal name="VC read" expl="VC for read" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC write" expl="VC for write" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> - </goal> - <goal name="VC const" expl="VC for const" proved="true"> - <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof> - </goal> -</theory> -</file> -<file name="../imp_test.mlw"> -<theory name="Imp_test"> - <goal name="ex1" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="82"/></proof> - </goal> - <goal name="ex2" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="101"/></proof> - </goal> - <goal name="ex3" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="97"/></proof> - <proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof> - </goal> - <goal name="ex4"> - <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof> - </goal> - <goal name="ex5"> - <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof> - </goal> - <goal name="ex6"> - <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="74"/></proof> - </goal> - <goal name="ex7"> - <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="84"/></proof> - </goal> - <goal name="ex8"> - <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="100"/></proof> - </goal> -</theory> -</file> -<file name="../imp_ex_assignment.mlw"> -<theory name="Imp_ex"> - <goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true"> - <proof prover="0"><result status="valid" time="0.68" steps="783"/></proof> - </goal> - <goal name="VC beval_ex" expl="VC for beval_ex" proved="true"> - <proof prover="0"><result status="valid" time="0.20" steps="667"/></proof> - </goal> - <goal name="VC ceval_ex" expl="VC for ceval_ex"> - <transf name="split_vc" > - <goal name="VC ceval_ex.0" expl="postcondition" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="74"/></proof> - </goal> - <goal name="VC ceval_ex.1" expl="postcondition"> - <proof prover="0"><result status="timeout" time="1.00"/></proof> - </goal> - <goal name="VC ceval_ex.2" expl="postcondition"> - <proof prover="0"><result status="timeout" time="1.00"/></proof> - </goal> - <goal name="VC ceval_ex.3" expl="postcondition"> - <proof prover="0"><result status="timeout" time="1.00"/></proof> - </goal> - <goal name="VC ceval_ex.4" expl="postcondition"> - <proof prover="0"><result status="timeout" time="1.00"/></proof> - </goal> - </transf> - </goal> -</theory> -</file> -<file name="../imp_ex.mlw" proved="true"> -<theory name="Imp_Ex" proved="true"> - <goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true"> - <proof prover="0"><result status="valid" time="0.52" steps="783"/></proof> - </goal> - <goal name="VC beval_ex" expl="VC for beval_ex" proved="true"> - <proof prover="0"><result status="valid" time="0.22" steps="667"/></proof> - </goal> - <goal name="VC ceval_ex" expl="VC for ceval_ex" proved="true"> - <proof prover="0"><result status="valid" time="0.08" steps="237"/></proof> - </goal> -</theory> -</file> -<file name="../imp.mlw" proved="true"> -<theory name="Imp" proved="true"> - <goal name="ceval_deterministic_aux" proved="true"> - <transf name="induction_pr" proved="true" > - <goal name="ceval_deterministic_aux.0" proved="true"> - <proof prover="0"><result status="valid" time="0.05" steps="135"/></proof> - </goal> - <goal name="ceval_deterministic_aux.1" proved="true"> - <proof prover="0"><result status="valid" time="0.08" steps="180"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2" proved="true"> - <transf name="induction_pr" proved="true" > - <goal name="ceval_deterministic_aux.2.0" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.1" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.2" proved="true"> - <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof> - <proof prover="1"><result status="valid" time="0.11"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.3" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.4" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.5" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof> - </goal> - <goal name="ceval_deterministic_aux.2.6" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof> - </goal> - </transf> - </goal> - <goal name="ceval_deterministic_aux.3" proved="true"> - <transf name="induction_pr" proved="true" > - <goal name="ceval_deterministic_aux.3.0" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.1" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.2" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.3" proved="true"> - <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof> - <proof prover="1"><result status="valid" time="0.06"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.4" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.5" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="85"/></proof> - </goal> - <goal name="ceval_deterministic_aux.3.6" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof> - </goal> - </transf> - </goal> - <goal name="ceval_deterministic_aux.4" proved="true"> - <transf name="induction_pr" proved="true" > - <goal name="ceval_deterministic_aux.4.0" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.1" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.2" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.3" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.4" proved="true"> - <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof> - <proof prover="1"><result status="valid" time="0.06"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.5" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof> - </goal> - <goal name="ceval_deterministic_aux.4.6" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof> - </goal> - </transf> - </goal> - <goal name="ceval_deterministic_aux.5" proved="true"> - <proof prover="0"><result status="valid" time="0.05" steps="133"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6" proved="true"> - <transf name="induction_pr" proved="true" > - <goal name="ceval_deterministic_aux.6.0" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.1" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.2" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.3" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.4" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.5" proved="true"> - <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof> - </goal> - <goal name="ceval_deterministic_aux.6.6" proved="true"> - <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof> - <proof prover="1"><result status="valid" time="0.11"/></proof> - </goal> - </transf> - </goal> - </transf> - </goal> - <goal name="ceval_deterministic" proved="true"> - <proof prover="0"><result status="valid" time="0.03" steps="107"/></proof> - </goal> - <goal name="VC beval"> - <proof prover="0"><result status="valid" time="0.02" steps="73"/></proof> - </goal> - <goal name="VC aeval"> - <proof prover="0"><result status="valid" time="0.01" steps="73"/></proof> - </goal> -</theory> -</file> -</why3session> diff --git a/imp_test/why3shapes.gz b/imp_test/why3shapes.gz index 527dbbaaa0a8756a227cdfe895f87a3dc77d2479..e77ae85f75ada1fa5f828574133cb1a1c57611fd 100644 Binary files a/imp_test/why3shapes.gz and b/imp_test/why3shapes.gz differ diff --git a/imp_test/why3shapes.gz.bak b/imp_test/why3shapes.gz.bak deleted file mode 100644 index f0927eda25523e6df29d23ed01f9d1f0349555b8..0000000000000000000000000000000000000000 Binary files a/imp_test/why3shapes.gz.bak and /dev/null differ