From 6e6adc8105a6c36d71aa88c33fab55f3b8cd7c05 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Tue, 2 Oct 2018 09:08:35 +0200
Subject: [PATCH] polished imp_test
---
imp_test/why3session.xml | 240 +++--------------------------------
imp_test/why3session.xml.bak | 238 ----------------------------------
imp_test/why3shapes.gz | Bin 3238 -> 322 bytes
imp_test/why3shapes.gz.bak | Bin 3230 -> 0 bytes
4 files changed, 18 insertions(+), 460 deletions(-)
delete mode 100644 imp_test/why3session.xml.bak
delete mode 100644 imp_test/why3shapes.gz.bak
diff --git a/imp_test/why3session.xml b/imp_test/why3session.xml
index a511523..1e004b5 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 428557c..0000000
--- 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
GIT binary patch
literal 322
zcmb2|=3oGW|Fx6OdpjHQG`xSm{zh!epRCJGT)R1#&+qQ=n6=HIz}mw6+w<RY#T}QQ
zYcAouKYaq5Q!lTe^lGCSSDieR8a8rX*|y>Ax_rOx>dj?a%x~A<xRkZ^>AMZ3Hta=m
zAtt*wyJk#r305u8&}}z7KIgJddcB5yqPQBLSd*~=qqskp@2Z5C0!8Xy=2c9q+)^HW
z_5H_;7XcHl?5)&VaE;eyMW#HfXyj9_t!<J)b(`KkGby#Ze|MkHv6Zi^96l{`l3KIG
zEwJjO?viD9I=el7`X{WPZKXeB)nbP=iAN2#SrnfVT^-@t<0N-iCys?b{^PMsUcJ?)
zKhL=EctUe@@(GD5A;U~dE0wN|RnN0t&i?fK&gC=D71yr}xUt#!nvZG8<B!k32nDB!
eZ#Yrq8vFRnr%%s6W$(CD%cQ3LD{~7I0|Nk`Ihy1E
literal 3238
zcmb2|=3oGW|8HeZ=gA!ZxG#QTb;5$xtA7PL$hasuI5<p*>DkHBc)`ED!`JfBsY}n7
zSDl#qGVa|Z??TzgO(hTf&R<#lI@a{Ic2e-<@>5psw^W$#8CRXNn~~AHT7Ox$_}90)
z#qFoPEjzqKx8>BTUr8LfuCuo;h@QQgv#soaIj=;c&aI#=AD2}~Td;F<CNU+t-F(wf
zzwcMXdb@o;p6}l#y;#asK3jKLSoZ3^Cq8P?TDxW(vO6_@zp%<uUZISI=awdD-dj9b
zn|ES!Z)>^7%eP<8n#IJLpLu`y&{m!8dG`OUUUI6JS~mXKd1r#Y<BsJMcz3<plqkHl
zV_xsmIS1aa*sraaZ!S`Fj<I{y$<X;HCVO2~IpyJaL7cU=qI|3F?cQ{aWgE_){5_-D
z&rmESozqfc&94vFq*uF_<(gPTGb~t8yu#^3V6$3K0{6<8IGq;@|47wwIsILlW4mWh
z-T&gI+x&A29-k=ml31g4Yx3vF)k|EKyIni*rvK8;N_qDr>scE(kEw(#5Iy#+qSeT8
z&8dQ`6ILBxY*Nqr{?O|^dH(sUx)#KGss3CMv%*pJ@sZ3{N4AnJ?pZ<Z8XxaFJrC+l
zuAX(r?PrLJ-W<-0;<+o`^p1(EZ#(EABA+C1FXriEo?F3*4htRFlodFmZ#asHGi_Kh
z*;ny~Z1es*wf{6<da73K-L1=AyEAdJljG5ZRq9+JH`JbPZAo1<qd9)%9rN<rpWmu|
zU%9HIb8^ygtJzv{zN_4{Un)-I61yvRm9vk-pS^Yd6}jCpN4Bcmb6qQN(&6m1sb!N=
zCMa#Z&3gFE8{eNhg8wclKQ;fs*P~VChoXO4?NEKeI_+8SH~;r0djgD4Po1keyXwK)
z+vefdl{z{8Y}<C4^UAxf__BtN*Ufpwuc-KKP=0aE+x~K${oVT~%U8#2h<jzZV_9a?
z>FMIPqXoBb-xPDD^5?>Hr}?=ZKM2pLU*oNQx>{(ZU|af(nU}d1vrF(=TfM(s7AKdy
zK9lM8!i75TH*Qz%nVI<Q#&5x6Z(p2w^Ik*lHp?r|&s{wVr~mpY^cq+k?wRdieQ1X4
z-1gFjI;X1(EhFD;RyRHLfya20y6pjhH!s#$Rn*6Drl=p{yM5x*J-t61kJDxpio5k1
z>{<MIgHX@BjxZDEO?T4sGg=Nxrlsv?oc3p3&las9Yb}?Alb&%w85|t3JA1wxyVy)o
zJjDP0-t-SyxBsm(*FWrUUbOw3{Oh-`x8L3|;ot|aYqclZUhlD6_ViRs_@^c1k5*f=
z*_XuZcG;ZL@nO}U?}B^m>+h#dyerxsZa-Dk_ROK&_e%tKpLxAYU)JGt+-8rhAO9*W
z6V{U7C8Feb`={&+$wV>VJ9)=!{9==4%PrHJ=$qWMsP)(B$1TrQz6w0FbS>3%KFe`>
z+w<<XYnN^BzGr6mY7KMvOO;L6*Xk}~xpr)U&on*0>D%6%JFn+-Yv=Tk%iXj8$Nb%N
z?`8J<HP@3`A1d9s6Z5x1H!SYs-PgNY=bm|@7q8!+v1z)~?%b`<**7$GSUvc3&C!Zs
zFO$P+`RV0-BI4I~?pSqME_AoEP;G3@kMC1gEZgaD`pMmSw{G2eyyBY#!#j^NxBiAb
z-+%RIe(AsHx&Oh;^U=?5TeCb@C{{fmlikyLA|=1sX|n8_>p#~Wd%2M5ZP&kobj^3l
zcQW3VWv|=!c<t7hxV)M#=a^1>kxg<jxD$8GVEKf_BIlj->nf`^`{u9zeD&L_w_o4N
z-JVdpd+F@AYP)0Bur3O5Sh&h;)&n2Domv_CTl)k(7FNHUQpVKU|M0O|^?V+Uc*PCv
zE4H3HR?&XIQd9WUN)=aW<Go?=p`wz;6_er)thjKmr(n~iM!|zCzpTqrR%gj}<jz>5
zYudc>+^aLJN?!l87FpO#eUQ^JGs!S=N^DZ~?J15|R`Oatz0h17IBUB2T-L&u^P>26
zz6t+Tw0N@@UozX-jHO#mq>5MQsg_+WKBcYd*<~HWd8AV>{(Iggy$9EBthYY$P3%JQ
zrWGC=x!&^5Tf6D%oVlymY^HD7w|8<_apn(?3Ax8Rs@$^AYyFPQpS{>OuQ(w!XpN%!
zCC%_;Ej2^Orf<jm<_J{YZJS+l|KG1X>7c&qx?-7?b^Lh&{9k(Y&#c|}PJVUT;=5hd
zRu{hf`NStY``YgGW$$}3&rRFA?n&5o@5)tdF)=S*-PAYh+<TQHs<CUy38~}jCiKar
z-fDPL#r)Ch)c2S>jIlq`&dDVd@QM8{n{BrE(UA?Se;=|jdaxow<_ib&yTYrUg$1tz
z471P2^1Zs)taP=Z+P_qlP2MPY;uYnE&2~j!u2#KQT5@V>xa@%qkNf!L1Lis0V0?7$
zaqaB0VWvEK`O^>Oq-I#JyJM!W>vbUV=Ch&?5;DGq59GqvT?vhQu`BZCoy(=oMQ<0x
z)W`2MbNFQVdX7r*q)QRW6St-=&zU4+q)~onqg+Xe!|q*2f7o@%mfWtI;MktfZ+%Kp
z&Us76qdPC!vnEbg&25m1__$!!ysHa6gazzh?7Xk(zo%f*ggHM}B%e64boz?PX>L*y
zcird8E%M`!zQFG?w<o%)(@Jt%ip%BND=!^qR&`j_D!j6AUmqy7MB?DgCA~+Y^;#Ds
zTx2}`S>|w`!X@#a(`H|NAoXtMyhQf%4-OjNQCgq7Zllfa?9b6twr~4WQM36*TBo!9
z@!0n#b+57IH!^<TA(`qFYt3j|ePZ8lo^y-X?o_9#e7NR4pZiS5DT}2yq(d)=G{gkd
z7pAe4Ug?{3?(XaT^;@TXS?1(*;HbLx-6EbRSzTVz!j{qh*BHHE>$pAhNZ-rdHw)u;
zPGXS{d^bIa?PBK4f}W|IKEbL_H2!9BN-SA=Y{oe$we7F=imU&dS@_6pLUYWKW!*2<
zwZF{$tGV<d-!A!zPk$BmiZA}NLAqAc)!3E$WYguqWo0ub8UKFO{Jg_xfzXA{&;Iw9
zorw&+f398I$R?BF)r*e;`4{eK>b|$y5PbX7uGinD-g>$$Xr)^FBZK80QYlRf1vGXq
z;Mo}N&OW1Wr?tu%Vf7h~pN^|bm}(^HU!S8@EyBG^Wb*mI@Lb7a6SLW6?-q%qe06yB
zHniU3mvO(shb?zjv(-N6s9sg(RdVEF%MrCG)yekh{p$)&dhUro%)B$0*GMktykuI(
zJWkn^qJ4^so|j&@J>Ssvz-6JN`K#E@U-$p;=MLYY%AQMlO3UUng}8TdZ8AJrUAIDS
zUefL7-}{$Ke7{r7V6(PbrY4EQsLqKi>9EmE_I9C^OP3~ZTrg*f*ox3hv-kyy=PsSB
z=Zg+dDy)^y2@Q2`U%B9j$H_Zci5q|HDJnP@_NRCX^HL+$*+;cED;u0Mkd9xwF=mSM
z>E~as_`h80UwHNYx|w!MUFPhc{ZHqpv!WYkmyg@RvlF!>qMMINF-4r(-<~(a?TnvE
z;m>NvZKv20_9{+YeEFu8#-kfjYo9Q^<lg%IhwGNZ$tiR7_Vk>}Wmv)GTJ$)_ac-^K
zY%Ryoqjjo(4SIK|uXYy|UZS^H{mQ|nGYxKbD{swMd&d8K?yP;LN1mU^G<h&D?@r7O
zt)*S74JAK$wPx^IC>s}6@BDQq^Ev+w!OIQRyHtC+bFx{dOx$dG)MwjVsiKwBmTa{w
zUi^_gv(x^n#MLPQ2RA)m;Qf2iiQSU~)=GFJUVNwhveSO6$_bIPTGxAyiSr5Woo409
zx<Z7f?eF$wKRz0Lw9f9b-`bGj=eS+i@RDj#kmuB>onDp;XK7p8d|crt?tFUT>xZ-F
zMeg~VyG8kS`E3Vx#>xE|Q<QiFQesy7O!B<><ezlEy2<nHw{N^Y_jU5F&whG#9swRN
zTyI`z<cSZqsjErv>D{~7zWUmpbe}s{6=rv4Up=^lE6Gv)a^DxG&StNWCfh<D3x#LG
z&l&!1u}nB|p#AC^|G>|W-D}(SY^wKp5n}3o<c#6#OXoKIRANr~_QWGI)_dx_Ur$~Y
zd0hDHC-W=wY3h$fA3pqhA>wTFulB`^CExdX+g=s88n)!Y?T;R7jv1sdUtGD!^z{;x
zxpBw&cHh~VKHE8_Zu7%u0-OEk=Y6@{75u;V`NNKD%U!;3-tYL9TF{a4x21z^zGL+L
zf5nV`YAXY}FEvIi?%ep~SB$$=_4m3Plh4_Dyj=eE-G?2_pETX-|E%benv-kutZ36k
z;U?ADlTG$+b8A?&#_*Ep_U4OXfwdFe>`$NhR(kvHE(T3yNsd6DvpYi)Ue?>T%sOGe
zy=H!~)t_Cbw@-O}<mfdS=Pdh-fP<mhy`kG8vdk);G1wfIsj^`DpWpoA;iS5Mo?l+;
zeT#ckU#F?QZ~COH|64extqoOuenHmh?tjO#_uglQq<AW;PGz`Kw;(t~dBGgRwvx`Y
sA3GnE2{&=|oMP{itVz&#`#gk6X41Af2|xaREc<M)ZpgVu(UXAz0I7&{=Kufz
diff --git a/imp_test/why3shapes.gz.bak b/imp_test/why3shapes.gz.bak
deleted file mode 100644
index f0927eda25523e6df29d23ed01f9d1f0349555b8..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001
literal 3230
zcmb2|=3oGW|8HZw`=yTy?)x16LQdkvs#oERg#w-ojjT;ilFq1dwA5L3-_UmVj{Nm=
zrJP>--I${3tCuQ!Pvi6c=2IG4YP(;l{ZdZWC%?$&CbLowRI8o8$u68*@b&1IU#_*k
z-yQ8w-5j~mjeFsyRr@4-w@o^$aeM9At1OGlk8JOq;SjxP>4J~TDx@vgIXsWEDEXvs
zR{r<%SMuI}KOW8he``%omQ3xMtuvz5u9eto9C<tF<WUj6?SFn+-&}HG0-MOY7_O<0
zY%MF>1uSnwRBYGWyLac^me;eleg3_{L-+L3x3A;X=VS!E=6rI#YH2N}l5K0wiO}i1
zvpb5u<mfzSsXP8Rma}s6CB^45D^|>k`RZA{HptX7{gUH0eYRg8-c<#gX`c`9Nt{3V
zyCJ)ep;%J7X`w;L#~rVHuP8@}J9&5I2-sc>U8Nev>@hQ0rR(F-O}10w5Bodr*e`PR
z@afs#?bUDWOIQ?oBJ|PWD*j{LWz#M`IU-o|Noz{ctn+VwTNvH`*b=%`wbkLt>KUrd
zW}(vjoH4BYj8{G9?Qbi8sP+BT&!~Xr4JTaPIj272nq+)y_Jl>9?;5Ty@hf<=zg2I^
ztRrRSJ41^CcBF+Xy%Y)Y@$;FGk{Kbo^sh71q1mr%q8xT>GxeA~5U~h8Xn9`FW?`75
zZ%TIQ!nqCm@9h1j`EbdkeYaw#v91djns2pG-%dlP^G4FqDA{bYQxRXP^}gS|TXIjU
z@`NetH=);-O_!!+JG^!F*r#P=_e+XzhhM>?55HbKR4-M~o4#b0@YX(oqdKP1VK0`P
zn9w)tuAXFCV*aV)b6=|8k*sf8ef{@p;oS4rFY0>gZ>b8~vcEe0Ve9P3dpCck1pDu)
z{Qc~go1YSUUG(kSoLAn-?tjDaczyn@xPZwl2m2P@-v8D3{rAhYzWZ*^=l+&o=(jF&
zR>I#;U(>3Ooc*S={`H<e0neYdw<`YNJY)aOTm5vkdXO^jd6UgcY<c-iIIQj7&$iO{
z?{v3qe7kL;&il^o%Dpo)`HuXac<k+uGmqX|%nNENaJrYTHsR?)p(XB8vohUOPxP6j
z9e<uEJz>5_>Fqf>{717*FMaSa?z(PqA>+o!o3|hQ%~Z~?&U{rS9eMBap?;IRWs+MB
zvX(rQo!{P@P;jYg|Jeo|{-e^imoE4icgHiXzQQ%DxGSlZ!^br$N8^&;g6!!Z>smXG
zYq|V*c=xwZT<)#=e~*^_cp0|t+RxPbpU>W^>E&qbnN&J|(?hlQ`LCbO<y`;7PyWdD
za;CZ$OUhc)Rth`}{rO(`_rE{2;jU%xE%y9csq-|^?#{D!CXc39#`62KUs!d$X34E5
zbpqEpr}M{hPF(W#5nsVQ19{&=dG{)3?S8VYZpQAEZF1aG;&$w}Ia{F@#BVsyJ0#rb
z%AUl)>blK0qpCLF$W^uFp4)sTwE9^T>(tDH5>1IqzoxQt>)bvXdCT>Bi!*!B!>@1a
z*VRj|Z@GQ@wS0cn^>ZbQx8Gj++DbO=*N6A7tyQmUzdU%3Nn~wPgOx!}sAHPrs=!(4
z7xn8Zt9J`NnX%sddVc;kt8LGAhrTS^d`eF|+wpaX!^Bl)vlKF-4dyqomH8WbEM#7s
zS-#+dVNFcx`_z_zeN74M9UU`zKlV9n*krVD&gq~vhM%+lhK5=uv#n?4mJn6B+c<gc
z&1~N1pLVb7ooleBRcFFRqren{tC44794^Ruik_T!F4e+1srpI&hNsdwKiQ)99h?SX
zuGygKc19v4p!|}|#@boSg(IY!jUsPZ${w0_T{iEg;?$>J_M1*u-Cwi9+2Hrzcdzmi
z)s1(4y;|h$Usl_mS5?VSEo8{PW;^30!3XmgqW(wRXAO#RO6Q)ywytcu=bKXYX;B<o
zyzafca_!kXmr@0W7007jCv9q2B^0cs*?d6F<d&wp+??)9Z{y$GHNCjV&G^Qy_=i=k
zk*e;7%tnzPCpw;5xNFLd(DRz_Ej>kVzMXnv?w4Pygcp6|zESml)$JR0tY4<+Xs(TD
zRd{e=+xZzqWviq<#9aD!S^MM7Bum}dx#}L@o4%bBul+Xt?8%HwhtQcK*(W@cPhFki
z<+&iNX+?~{2G2d=hkf_;E8kzK_;>YmbN4B)N(-7R7xXL4Nap!{d)3d3?T_a1n^^DP
zbKCRmtGl+B+h@#6UcG&4%&RR^c4yu2=8m89IBDvQXcY%mt*oVM3*U4dd*OLWY}0Gm
zBh_L1ra$Vtamc*<8;f(nh9BF5Z}qeZAAfgP{Mntw7dM#P5NzAK+*keTmA9LVx6O;@
ze|GTTgsdCY=Sx)C<c(e{DYq@*`+4HxcK=neEg?I<EMt~1dH3Xl;A75KS&er}_qHo-
zH$N=!sqAG+*sA-PkGCD#EYX;jJo~GFp~<eK8`ZaVT<WNJ_&P1Q`22O=V_TaG|JFXf
z#c=X?kLAghC89ySuGgl`-Q<~dBH>P8vP@3NkzF^6{!BQ+w=LJVdV}JP%Z)`o$0q0|
zS(qPN7<KM+keLJTq6!0F{Z|poI6LLv+{r#AtUpObRozZf!f4ThNu`(mE`6Llztkc{
zmQU*ebENubPQ6I=%bjOTZlufd9Xq1<`h&-{!ali^w*{0fCSUN__cX{vL`!0YjlRJf
z52d$vx8GXRcA?;W50AAA8~?<I(>~u4lRCZE+ULTiJ&kRbf1Z6bTb2Lsobp<g?J?4e
zSljk4zpJ5qSB~?6jAHvkW0r2IZ}*B9v*p)*6PwXFrO<1m`Kk$;3_Att3iDV>FZBnV
zyL<Ki{wV*dU`5pjk0$$WJGLO!H*lfh#LZvNXEo<7xRI1-J?;Io<Ia!01Z$4$i1(6K
zX%}tUc+vVwsIdFN)v5sk9=?XLCcfLA?VYavZ)W8qw@HhGjx0ZYG1mX`?_a@Di)C}{
zPdxeUS*7p(^P$17pjl~MVv|_gCt6Bo&Umw$f1dKhjZ$A`e)i`NezvOX_RoU-lJiU$
zO8-=xFwc-bq|<Czniie*_-%T?>(Hx9XUTLep0mhp0;gO1g3a8gGQPcf!f=_h{5ap|
zBb;d#KOYPCNbwW~WS_IG7UAC|GWooqcGNPN-m`9%Tb2r}X7|d^|CPLa{|62x|J8f5
zHn8_rpWo`&=~rx`xUn<r<dgF^Cu_$PO?u&8v7l_#!=B@3iW?;ti7)Es+IdId;%O_X
zx94XlJ;-F;s2}S5<gu`l{dV?;Hm;4`E}F{~?gqNE-kkBo*8Yn4`Hycue|&6tZtoWv
z27l*%XCEHVWBwYBIT31~A9zgiQP^uHHf8cPrmb2jpINOQDS7-W{^6vqyYPMU+Eqy<
zQ@A|)rkq(TF6Mncn|*rAqxp+vHKvwsh+Jf3&3jBT?eS{UY28IBKQ~SMr5W*SPQc%{
z2fkS9KKhjLYqJTztB9)RCbO=bzFkclO%<*R9C-Do+Tn23otv`0PXFR2y*<yCu=k>t
zd;3i*4WSzzVOfsVJh!WVDLwcwBl5X?oZC|~h7i}HqQ^OkXY3~XhB}8Hty8Ut=&wF+
z)~}`J5wEtMvzc`!WAC0<S;^as>}|zOYMGBrUy)gLqk3O)apLMJTI-IbYzfzL$vz-C
zv-5WQ>hp8U{xx(&@K>Mz-cmR*cddg_ky*f*TicH3#H><PoW;%DYtNzbFC;xA*opP@
zJmzWNTql;R3Pu)ASk&}R`{0rJw}eu<(xzssJ?3urkX!2iifNY!SKD9nfIk(pf6Q%s
z<e#f>LNlRS$t^%heQL<csjIgL#}=o$r`xT%{Pe=7FPA>}p0C;CY<g?6e|gq~%Z-!z
zQ>I)JQ8=+9EYe#wb@K0gn|Tc9wr9yKD6SE*dVlVyyCfHPOb@T@$q%MSANRlS*;)AE
z#ra0__m-2(Y)_<}-I`>uvZ><2$t}te3WWil(-Y3iF!#xP?kr}o%jJ{M`cP>6*fOo|
zPvHE8>tyWIO4iL(-g<v?n$Fuuv-p&TGjY~y1+rH*tvvru?>Jx8%}(a|*W%jrx%yu(
zKVNv{@%{Eb*Iy5IUn!Oi%vF`GskWK4%8=)#L&+)yBem9Ff9%R^p6J=$mYMu%Hm~{d
zmfBw>&HmYbf6eC|H<mho@`dp}!MC>`Ot|=?rH5@k<J$cHI~mj`hpcc-ywH=9q_fk`
ze1cxzy?*ygOW8GRq{`ZlGfy~Q`0H{1suhYijvbFVS5~F8;np*i1=p`}1WYw`3n;8M
zxFxhw|I$nGnK$?4?T;2$NWH}7Bobb%CmQi#eS5&<Z|8IGPoKlL|J^s;w^oH4O^;8w
z#V-|7aFuJrscBwk+w|r%h|h5DPk-<~SHSk(C4KwOy1QrZdH*{vf6DXC(j~X-O%86_
zy6TC{uJ!=_`hemO)l#C7r#w7W8}jTgXs$90I47}qql@vMeR-R?99h+#Hup)^Bxt-%
azw9I<6y;~|C!u`vFZo8M6UK_33=9BI`cpsv
--
GitLab