diff --git a/examples/compiler_noproof.mlw b/examples/compiler_noproof.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..cdf47dc105f9722d4626614e131b0266f8f28c10
--- /dev/null
+++ b/examples/compiler_noproof.mlw
@@ -0,0 +1,168 @@
+
+
+(*Imp to Vm compiler *)
+(**************************************************************************)
+
+(* Compiler for arithmetic expressions *)
+module Compile_aexpr
+
+ use int.Int
+ use list.List
+ use list.Length
+ use list.Append
+ use imp_per.Imp
+ use vm_per.Vm
+ use state.State
+
+ function compile_aexpr (a:aexpr) : code =
+ match a with
+ | Anum n -> iconst n
+ | Avar x -> ivar x
+ | Aadd a1 a2 -> compile_aexpr a1 ++ compile_aexpr a2 ++ iadd
+ | Asub a1 a2 -> compile_aexpr a1 ++ compile_aexpr a2 ++ isub
+ end
+
+ goal g_2_1 : (* 2 + 1 *)
+ let c_imp = Aadd (Anum 2) (Anum 1) in
+ let c_out = compile_aexpr c_imp in
+ c_out = iconst 2 ++ iconst 1 ++ iadd
+
+ goal g_a_1 : (* a + 1 *)
+ let c_imp = Aadd (Avar (Id 1)) (Anum 1) in
+ let c_out = compile_aexpr c_imp in
+ c_out = ivar (Id 1) ++ iconst 1 ++ iadd
+
+end
+
+
+(* Compiler for boolean expressions. *)
+module Compile_bexpr
+
+ use int.Int
+ use list.List
+ use list.Length
+ use list.Append
+ use imp_per.Imp
+ use vm_per.Vm
+ use state.State
+ use Compile_aexpr
+
+ function compile_bexpr (b:bexpr) (cond:bool) (ofs:ofs) : code =
+ match b with
+ | Btrue -> if cond then ibranch ofs else Nil
+ | Bfalse -> if cond then Nil else ibranch ofs
+ | Bnot b1 -> compile_bexpr b1 (not cond) ofs
+ | Band b1 b2 ->
+ let c2 = compile_bexpr b2 cond ofs in
+ let ofs = if cond then length c2 else ofs + length c2 in
+ compile_bexpr b1 false ofs ++ c2
+
+ | Beq a1 a2 -> compile_aexpr a1 ++ compile_aexpr a2 ++
+ if cond then ibeq ofs else ibne ofs
+ | Ble a1 a2 -> compile_aexpr a1 ++ compile_aexpr a2 ++
+ if cond then ible ofs else ibgt ofs
+ end
+end
+
+module Compile_com
+
+ use int.Int
+ use list.List
+ use list.Length
+ use list.Append
+ use imp_per.Imp
+ use vm_per.Vm
+ use state.State
+ use Compile_aexpr
+ use Compile_bexpr
+
+ function compile_com (cmd: com) : code =
+ match cmd with
+ | Cskip -> Nil
+ | Cassign x a -> compile_aexpr a ++ isetvar x
+ | Cseq cmd1 cmd2 -> compile_com cmd1 ++ compile_com cmd2
+ | Cif bexpr cmd1 cmd2 ->
+ let code_false = compile_com cmd2 in
+ let code_true = compile_com cmd1 ++ ibranch (length code_false) in
+ compile_bexpr bexpr false (length code_true) ++
+ code_true ++
+ code_false
+ | Cwhile test body ->
+ let code_body = compile_com body in
+ let body_length = length code_body + 1 in
+ let code_test = compile_bexpr test false body_length in
+ let ofs = length code_test + body_length in
+ code_test ++ code_body ++ ibranch (- ofs)
+ end
+
+ function compile_program (prog : com) : code =
+ compile_com prog ++ ihalt
+
+ goal g1 : (* a := 2 + 1 *)
+ let c_in = Cassign (Id 1) (Aadd (Anum 2) (Anum 1)) in
+ let c_out =
+ iconst 2 ++
+ iconst 1 ++
+ iadd ++
+ isetvar (Id 1) ++
+ ihalt in
+ compile_program c_in = c_out
+
+ goal g2 : (* IF TRUE THEN a := 1 ELSE a := 2 END *)
+ let c_in = Cif Btrue (Cassign (Id 1) (Anum 1)) (Cassign (Id 1) (Anum 2)) in
+ let c_out =
+ (* <-- condition trivial true *)
+ iconst 1 ++ (* <-- then branch *)
+ isetvar (Id 1) ++
+ ibranch 2 ++
+ iconst 2 ++ (* <-- else branch *)
+ isetvar (Id 1) ++
+ ihalt
+ in
+ compile_program c_in = c_out
+
+ goal g3 : (* IF NOT TRUE THEN a := 1 ELSE a := 2 END *)
+ let c_in = Cif (Bnot Btrue) (Cassign (Id 1) (Anum 1)) (Cassign (Id 1) (Anum 2)) in
+ let c_out =
+ ibranch 3 ++ (* <-- condition trivial false *)
+ iconst 1 ++ (* <-- then branch *)
+ isetvar (Id 1) ++
+ ibranch 2 ++
+ iconst 2 ++ (* <-- else branch *)
+ isetvar (Id 1) ++
+ ihalt
+ in
+ compile_program c_in = c_out
+
+ goal g4 : (* IF a <= 0 THEN a := 1 ELSE a := 2 END *)
+ let c_in = Cif (Ble (Avar (Id 1)) (Anum 0)) (Cassign (Id 1) (Anum 1)) (Cassign (Id 1) (Anum 2)) in
+ let c_out =
+ ivar (Id 1) ++ (* <-- a <= 0 condition *)
+ iconst 0 ++
+ ibgt 3 ++
+ iconst 1 ++ (* <-- then branch *)
+ isetvar (Id 1) ++
+ ibranch 2 ++
+ iconst 2 ++ (* <-- else branch *)
+ isetvar (Id 1) ++
+ ihalt
+ in
+ compile_program c_in = c_out
+
+ (* simple sum program : *)
+ goal g5 : (* X := 1; WHILE NOT (Y <= 0) DO X := X + Y; Y := Y - 1 DONE *)
+ let x = Id 0 in
+ let y = Id 1 in
+ let cond = Bnot (Ble (Avar y) (Anum 0)) in
+ let body1 = Cassign x (Aadd (Avar x) (Avar y)) in
+ let body2 = Cassign y (Asub (Avar y) (Anum 1)) in
+ let lp = Cwhile cond (Cseq body1 body2) in
+ let code = Cseq (Cassign x (Anum 1)) lp in
+
+ let c_out =
+ (* your code here *)
+ ihalt in
+ compile_program code = c_out
+
+end
+
diff --git a/examples/compiler_noproof/why3session.xml b/examples/compiler_noproof/why3session.xml
new file mode 100644
index 0000000000000000000000000000000000000000..a96c43a7e5379301bfd85388fc04a46a17510c4e
--- /dev/null
+++ b/examples/compiler_noproof/why3session.xml
@@ -0,0 +1,300 @@
+<?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="Z3" version="4.7.1" alternative="counterexamples" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Eprover" version="2.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<file name="../imp_per.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="3"><result status="valid" time="0.01" steps="42"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="79"/></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="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.2" proved="true">
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></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="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.3" proved="true">
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></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="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.4" proved="true">
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic_aux.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="47"/></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="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.6" proved="true">
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="25"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../compiler_noproof.mlw">
+<theory name="Compile_aexpr" proved="true">
+ <goal name="g_2_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ <goal name="g_a_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ </goal>
+</theory>
+<theory name="Compile_com">
+ <goal name="g1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="44"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ <goal name="g3" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ <goal name="g4" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="g4.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="9"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="g5">
+ <proof prover="2"><result status="timeout" time="1.00"/></proof>
+ <proof prover="3"><result status="timeout" time="1.00"/></proof>
+ <transf name="compute_in_goal" >
+ <goal name="g5.0">
+ </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+<file name="../vm_per.mlw" proved="true">
+<theory name="ReflTransClosure" proved="true">
+ <goal name="transition_star_one" proved="true">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="transition_star_transitive" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="transition_star_transitive.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.00" steps="5"/></proof>
+ </goal>
+ <goal name="transition_star_transitive.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="Vm" proved="true">
+ <goal name="codeseq_at_app_right" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="30"/></proof>
+ </goal>
+ <goal name="codeseq_at_app_left" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="59"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="2"><result status="valid" time="0.13"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="27"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="90"/></proof>
+ </goal>
+ <goal name="cs_3" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_3.0" proved="true">
+ <proof prover="0"><result status="valid" time="2.72"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="56"/></proof>
+ </goal>
+ <goal name="g2_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="155"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="3"><result status="valid" time="0.04" steps="68"/></proof>
+ </goal>
+ <goal name="g3_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.07" steps="183"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="3"><result status="valid" time="0.07" steps="193"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test2" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="110"/></proof>
+ </goal>
+ <goal name="cs_3" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="263"/></proof>
+ </goal>
+ <goal name="cs_4" proved="true">
+ <proof prover="0"><result status="valid" time="0.14"/></proof>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="62"/></proof>
+ </goal>
+ <goal name="g2_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.06" steps="187"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="74"/></proof>
+ </goal>
+ <goal name="g3_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.09" steps="215"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="77"/></proof>
+ </goal>
+ <goal name="g4_trans" proved="true">
+ <proof prover="2"><result status="valid" time="0.24"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="2"><result status="valid" time="0.21"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test3" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="29"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="23"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/compiler_noproof/why3session.xml.bak b/examples/compiler_noproof/why3session.xml.bak
new file mode 100644
index 0000000000000000000000000000000000000000..36d5bc922ccfef269f36ce160cf0553cadf10a2b
--- /dev/null
+++ b/examples/compiler_noproof/why3session.xml.bak
@@ -0,0 +1,298 @@
+<?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="Z3" version="4.7.1" alternative="counterexamples" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Eprover" version="2.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<file name="../imp_per.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="3"><result status="valid" time="0.01" steps="42"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="79"/></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="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.2" proved="true">
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></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="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.3" proved="true">
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></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="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.4" proved="true">
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic_aux.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="47"/></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="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.6" proved="true">
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="25"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../compiler_noproof.mlw">
+<theory name="Compile_aexpr" proved="true">
+ <goal name="g_2_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ </goal>
+ <goal name="g_a_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ </goal>
+</theory>
+<theory name="Compile_com">
+ <goal name="g1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="44"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ <goal name="g3" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ <goal name="g4" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="g4.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="9"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="g5">
+ <proof prover="2"><result status="timeout" time="1.00"/></proof>
+ <proof prover="3"><result status="timeout" time="1.00"/></proof>
+ <transf name="compute_in_goal" >
+ <goal name="g5.0">
+ </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+<file name="../vm_per.mlw" proved="true">
+<theory name="ReflTransClosure" proved="true">
+ <goal name="transition_star_one" proved="true">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="transition_star_transitive" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="transition_star_transitive.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.00" steps="5"/></proof>
+ </goal>
+ <goal name="transition_star_transitive.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="Vm" proved="true">
+ <goal name="codeseq_at_app_right" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="30"/></proof>
+ </goal>
+ <goal name="codeseq_at_app_left" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="59"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="2"><result status="valid" time="0.13"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="27"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="90"/></proof>
+ </goal>
+ <goal name="cs_3" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_3.0" proved="true">
+ <proof prover="0"><result status="valid" time="2.72"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="56"/></proof>
+ </goal>
+ <goal name="g2_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="155"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="3"><result status="valid" time="0.04" steps="68"/></proof>
+ </goal>
+ <goal name="g3_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.07" steps="183"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="3"><result status="valid" time="0.07" steps="193"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test2" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="110"/></proof>
+ </goal>
+ <goal name="cs_3" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="263"/></proof>
+ </goal>
+ <goal name="cs_4" proved="true">
+ <proof prover="0"><result status="valid" time="0.14"/></proof>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="62"/></proof>
+ </goal>
+ <goal name="g2_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.06" steps="187"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="74"/></proof>
+ </goal>
+ <goal name="g3_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.09" steps="215"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="77"/></proof>
+ </goal>
+ <goal name="g4_trans" proved="true">
+ <proof prover="2"><result status="valid" time="0.24"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="2"><result status="valid" time="0.21"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test3" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="29"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="23"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/compiler_noproof/why3shapes.gz b/examples/compiler_noproof/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..897e5bf6906611286c7048c79c74f76b21d628e6
Binary files /dev/null and b/examples/compiler_noproof/why3shapes.gz differ
diff --git a/examples/compiler_noproof/why3shapes.gz.bak b/examples/compiler_noproof/why3shapes.gz.bak
new file mode 100644
index 0000000000000000000000000000000000000000..897e5bf6906611286c7048c79c74f76b21d628e6
Binary files /dev/null and b/examples/compiler_noproof/why3shapes.gz.bak differ
diff --git a/examples/imp_per.mlw b/examples/imp_per.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..52ce429feaccd38c0be2427f2009416ebfcd980e
--- /dev/null
+++ b/examples/imp_per.mlw
@@ -0,0 +1,86 @@
+theory Imp
+
+ use state.State
+ use bool.Bool
+ use int.Int
+
+
+ (* ************************ SYNTAX ************************ *)
+ type aexpr =
+ | Anum int
+ | Avar id
+ | Aadd aexpr aexpr
+ | Asub aexpr aexpr
+
+ type bexpr =
+ | Btrue
+ | Bfalse
+ | Bnot bexpr
+ | Beq aexpr aexpr
+ | Ble aexpr aexpr
+ | Band bexpr bexpr
+
+ type com =
+ | Cskip
+ | Cassign id aexpr
+ | Cseq com com
+ | Cif bexpr com com
+ | Cwhile bexpr com
+
+
+ (* ************************ SEMANTICS ************************ *)
+ function aeval (st:state) (e:aexpr) : int =
+ match e with
+ | Anum n -> n
+ | Avar x -> st[x]
+ | Aadd e1 e2 -> aeval st e1 + aeval st e2
+ | Asub e1 e2 -> aeval st e1 - aeval st e2
+ end
+
+ function beval (st:state) (b:bexpr) : bool =
+ match b with
+ | Btrue -> true
+ | Bfalse -> false
+ | Bnot b' -> notb (beval st b')
+ | Beq a1 a2 -> aeval st a1 = aeval st a2
+ | Ble a1 a2 -> aeval st a1 <= aeval st a2
+ | Band b1 b2 -> andb (beval st b1) (beval st b2)
+
+ end
+
+ inductive ceval state com state =
+ (* skip *)
+ | E_Skip : forall m. ceval m Cskip m
+
+ (* assignement *)
+ | E_Ass : forall m a x. ceval m (Cassign x a) m[x <- aeval m a]
+
+ (* sequence *)
+ | E_Seq : forall cmd1 cmd2 m0 m1 m2.
+ ceval m0 cmd1 m1 -> ceval m1 cmd2 m2 -> ceval m0 (Cseq cmd1 cmd2) m2
+
+ (* if then else *)
+ | E_IfTrue : forall m0 m1 cond cmd1 cmd2. beval m0 cond ->
+ ceval m0 cmd1 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
+
+ | E_IfFalse : forall m0 m1 cond cmd1 cmd2. not beval m0 cond ->
+ ceval m0 cmd2 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
+
+ (* while *)
+ | E_WhileEnd : forall cond m body. not beval m cond ->
+ ceval m (Cwhile cond body) m
+
+ | E_WhileLoop : forall mi mj mf cond body. beval mi cond ->
+ ceval mi body mj -> ceval mj (Cwhile cond body) mf ->
+ ceval mi (Cwhile cond body) mf
+
+
+ (* Determinstic semantics *)
+ lemma ceval_deterministic_aux : forall c mi mf1. ceval mi c mf1 ->
+ forall mf2. ([@inversion] ceval mi c mf2) -> mf1 = mf2
+
+ lemma ceval_deterministic : forall c mi mf1 mf2.
+ ceval mi c mf1 -> ceval mi c mf2 -> mf1 = mf2
+
+end
+
diff --git a/examples/state.mlw b/examples/state.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..a65547711f8bfaa9ba5d0541b7d91f58d53f1207
--- /dev/null
+++ b/examples/state.mlw
@@ -0,0 +1,45 @@
+
+module State
+
+ use int.Int
+
+ type id = Id int
+ type state = id -> int
+
+ let function get (f: state) (x: id) = f x
+
+ let function set (f: state) (x: id) (v: int) : state =
+ fun (y: id) ->
+ match (x, y) with
+ | (Id xv, Id yv) -> if xv = yv then v else (f y)
+ end
+ meta rewrite_def function set
+
+ let function ([]) f x = f x
+ let function ([<-]) f x v = set f x v
+
+ let function const (v: int) : state
+ ensures { forall x. result[x] = v }
+ = fun _ -> v
+
+end
+
+module Reg
+
+ use int.Int
+
+ type idr = int
+ type regs = idr -> int
+
+ let function read (f: regs) (x: idr) = f x
+
+ let function write (f: regs) (x: idr) (v: int) : regs =
+ fun (y: idr) -> if x = y then v else (f y)
+
+ meta rewrite_def function write
+
+ let function const (v: int) : regs
+ ensures { forall x. read result x = v }
+ = fun _ -> v
+
+end
\ No newline at end of file
diff --git a/examples/vm_ind.mlw b/examples/vm_ind.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..752c229551c81ce568f1e45726874d1d462ba940
--- /dev/null
+++ b/examples/vm_ind.mlw
@@ -0,0 +1,110 @@
+module ReflTransClosure
+
+ type parameter
+ type state
+ predicate transition parameter state state
+
+ inductive transition_star parameter (x y : state) =
+ | Refl_ : forall p x. transition_star p x x
+ | Step: forall p x y z.
+ transition p x y -> transition_star p y z -> transition_star p x z
+
+ lemma transition_star_one: forall p s1 s2.
+ transition p s1 s2 -> transition_star p s1 s2
+
+ lemma transition_star_transitive: forall p s1 s2 s3.
+ transition_star p s1 s2 -> transition_star p s2 s3 ->
+ transition_star p s1 s3
+
+end
+
+
+theory VM_ind
+
+ use export int.Int
+ use export list.List
+ use export list.NthNoOpt
+ use export state.State
+
+ type stack = list int
+ type pos = int
+ type machine_state = (pos, stack, state)
+
+ type instr =
+ | Iconst int (* push n on stack *)
+ | Ivar id (* push the value of variable *)
+ | Iadd (* pop two values, push their sum *)
+ | Isub (* pop two values, push their difference *)
+ | Ihalt (* end of program *)
+
+ type code = list instr
+
+ function pop (st : stack) : (int, stack) =
+ match st with
+ | Nil -> (0, st)
+ | Cons c st' -> (c, st')
+ end
+
+ function push (v : int) (st : stack) : stack = Cons v st
+
+ inductive transition code machine_state machine_state =
+ | trans_const: forall c p n. nth p c = (Iconst n) ->
+ forall s m. transition c (p, s, m) (p + 1, push n s, m)
+
+ | trans_var: forall c p id. nth p c = (Ivar id) ->
+ forall s m. transition c (p, s, m) (p + 1, push m[id] s, m)
+
+ | trans_add: forall c p. nth p c = (Iadd) ->
+ forall n1 n2 s m. transition c (p, push n2 (push n1 s), m) (p + 1, push (n1 + n2) s, m)
+
+ | trans_sub: forall c p. nth p c = (Isub) ->
+ forall n1 n2 s m. transition c (p, push n2 (push n1 s), m) (p + 1, push (n1 - n2) s, m)
+
+
+ clone export ReflTransClosure with type parameter = code,
+ type state = machine_state, predicate transition = transition
+
+ predicate vm_terminates (c:code) (mi mf:state) =
+ exists p. nth p c = Ihalt /\
+ transition_star c (0, Nil, mi) (p, Nil, mf)
+
+ predicate vm_terminates_non_empty (c:code) (mi mf:state) =
+ exists p s. nth p c = Ihalt /\
+ transition_star c (0, Nil, mi) (p, s, mf)
+
+end
+
+theory VM_ind_test
+
+ use VM_ind
+ use map.Const
+
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ constant m0 : state = (const 0)[Id 1 <- 2]
+ constant c : code = (Ivar (Id 1) :: (Iconst 1 :: (Iadd :: (Ihalt :: Nil))))
+
+ lemma c0 : nth 0 c = Ivar (Id 1)
+ lemma c1 : nth 1 c = Iconst 1
+ lemma c2 : nth 2 c = Iadd
+ lemma c3 : nth 3 c = Ihalt
+
+ lemma g1 : (* 2 + 1 = 3, step one *)
+ transition c (0, Nil, m0) (1, 2 :: Nil, m0)
+
+ lemma g2 : (* 2 + 1 = 3, step two *)
+ transition c (1, 2 :: Nil, m0) (2, 1 :: (2 :: Nil), m0)
+
+ lemma g3 : (* 2 + 1 = 3, step three *)
+ transition c (2, 1 :: (2 :: Nil), m0) (3, 3 :: Nil, m0)
+
+ lemma g3_trans : (* 2 + 1 = 3, multiple steps *)
+ transition_star c (0, Nil, m0) (3, 3 :: Nil, m0)
+
+ goal g_term : (* 2 + 1 = 3, terminates with non-empty stack *)
+ vm_terminates_non_empty c m0 m0
+
+end
+
+
+
diff --git a/examples/vm_mem.mlw b/examples/vm_mem.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..25ac783e84c51c9e062f66785e5c63904972dc56
--- /dev/null
+++ b/examples/vm_mem.mlw
@@ -0,0 +1,103 @@
+theory VM_mem
+
+ use export int.Int
+ use export list.List
+ use export state.State
+
+ type stack = list int
+ type machine_state = (stack, state)
+
+ type instr =
+ | Iconst int (* push n on stack *)
+ | Ivar id (* push the value of variable *)
+ | Iadd (* pop two values, push their sum *)
+ | Isub (* pop two values, push their difference *)
+
+ function pop (st : stack) : (int, stack) =
+ match st with
+ | Nil -> (0, st)
+ | Cons c st' -> (c, st')
+ end
+
+
+ function push (v : int) (st : stack) : stack = Cons v st
+
+ function fconst (v : int) (m : machine_state) : machine_state =
+ let (stack, state) = m in (push v stack, state)
+
+ function fvar (id : id) (m : machine_state) : machine_state =
+ let (stack, state) = m in (push state[id] stack, state)
+
+
+ function fadd (m : machine_state) : machine_state =
+ let (stack, state) = m in
+ let (a1, st1) = pop stack in
+ let (a2, st2) = pop st1 in
+ (push (a1 + a2) st2, state)
+
+ function fsub (m : machine_state) : machine_state =
+ let (stack, state) = m in
+ let (a1, st1) = pop stack in
+ let (a2, st2) = pop st1 in
+ (push (a2 - a1) st2, state)
+
+end
+
+
+theory VM_mem_test
+
+ use VM_mem
+
+ goal g1 : (* 2 + 1 = 3 *)
+ forall state.
+ fadd (fconst 1 (fconst 2 (Nil, state))) = (Cons 3 Nil, state)
+
+ constant s0 : state = (const 0)[Id 1 <- 2]
+ constant m0 : machine_state = (Nil, s0)
+
+ goal g2 : (* a + 1 = 3, state[a] = 2 *)
+ fadd (fconst 1 (fvar (Id 1) m0)) = (Cons 3 Nil, s0)
+
+end
+
+
+theory VM_mem_list
+
+ use export VM_mem
+
+ function vm_i (i : instr) (m : machine_state) : machine_state =
+ match i with
+ | Iconst v -> fconst v m
+ | Ivar id -> fvar id m
+ | Iadd -> fadd m
+ | Isub -> fsub m
+ end
+
+ function vm (il : list instr) (m : machine_state) : machine_state =
+ match il with
+ | Nil -> m
+ | Cons i il' -> vm il' (vm_i i m)
+ end
+
+end
+
+theory VM_mem_list_test
+
+ use VM_mem_list
+
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ constant s0 : state = (const 0)[Id 1 <- 2]
+ constant m0 : machine_state = (Nil, s0)
+
+ goal g1 : (* 2 + 1 = 3 *)
+ vm (Iconst 2 :: (Iconst 1 :: (Iadd :: Nil))) m0 = (3 :: Nil, s0)
+
+ goal g2 : (* a + 1 = 3 *)
+ vm (Ivar (Id 1) :: (Iconst 1 :: (Iadd :: Nil))) m0 = (3 :: Nil, s0)
+
+
+end
+
+
+
diff --git a/examples/vm_mem/why3session.xml b/examples/vm_mem/why3session.xml
new file mode 100644
index 0000000000000000000000000000000000000000..2a1422bd9d0c936e66827fa92d8bea04a8e3f611
--- /dev/null
+++ b/examples/vm_mem/why3session.xml
@@ -0,0 +1,28 @@
+<?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"/>
+<prover id="2" name="Z3" version="4.7.1" alternative="counterexamples" timelimit="10" steplimit="0" memlimit="1000"/>
+<file name="../vm_mem.mlw">
+<theory name="VM_mem_test">
+ <goal name="g1">
+ <proof prover="0"><result status="unknown" time="0.06"/></proof>
+ <proof prover="1"><result status="timeout" time="1.00"/></proof>
+ <proof prover="2"><result status="timeout" time="10.00"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
+ </goal>
+</theory>
+<theory name="VM_mem_list_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="138"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="137"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/vm_mem/why3session.xml.bak b/examples/vm_mem/why3session.xml.bak
new file mode 100644
index 0000000000000000000000000000000000000000..1e7e84676d17432efa719ad004318d485477361e
--- /dev/null
+++ b/examples/vm_mem/why3session.xml.bak
@@ -0,0 +1,26 @@
+<?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="../vm_mem.mlw">
+<theory name="VM_mem_test">
+ <goal name="g1">
+ <proof prover="0"><result status="unknown" time="0.06"/></proof>
+ <proof prover="1"><result status="timeout" time="1.00"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
+ </goal>
+</theory>
+<theory name="VM_mem_list_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="138"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="137"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/vm_mem/why3shapes.gz b/examples/vm_mem/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..7861f4e60dd895c80d51205854aebe7f33b1657d
Binary files /dev/null and b/examples/vm_mem/why3shapes.gz differ
diff --git a/examples/vm_mem/why3shapes.gz.bak b/examples/vm_mem/why3shapes.gz.bak
new file mode 100644
index 0000000000000000000000000000000000000000..7861f4e60dd895c80d51205854aebe7f33b1657d
Binary files /dev/null and b/examples/vm_mem/why3shapes.gz.bak differ
diff --git a/examples/vm_per.mlw b/examples/vm_per.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..7928a575225babdd6a4cd1fb3913d3cc2f22d124
--- /dev/null
+++ b/examples/vm_per.mlw
@@ -0,0 +1,254 @@
+
+(* Utility module: reflexive transitive closure of a parameterized
+ relation. *)
+module ReflTransClosure
+
+ type parameter
+ type state
+ predicate transition parameter state state
+
+ inductive transition_star parameter (x y:state) =
+ | Refl_: forall p x. transition_star p x x
+ | Step: forall p x y z.
+ transition p x y -> transition_star p y z -> transition_star p x z
+
+ lemma transition_star_one: forall p s1 s2.
+ transition p s1 s2 -> transition_star p s1 s2
+
+ lemma transition_star_transitive: forall p s1 s2 s3.
+ transition_star p s1 s2 -> transition_star p s2 s3 ->
+ transition_star p s1 s3
+
+end
+
+
+(******************************************************************************)
+
+(* The machine operates on a code c (a fixed list of instructions)
+ and three variable components:
+ - a program counter, denoting a position in c
+ - a state assigning integer values to variables
+ - an evaluation stack, containing integers.
+*)
+
+theory Vm
+
+ use export state.State
+ use export int.Int
+ use export list.List
+ use export list.Length
+ use export list.Append
+ use export int.EuclideanDivision
+
+ type pos = int (* read position on stack *)
+ type stack = list int (* stack contains just integers *)
+ type machine_state = VMS pos stack state (* virtual machine configuration *)
+
+
+ type ofs = int
+ (* The instruction set of the machine. *)
+ type instr =
+ | Iconst int (* push n on stack *)
+ | Ivar id (* push the value of variable *)
+ | Isetvar id (* pop an integer, assign it to variable *)
+ | Ibranch ofs (* skip ofs instructions *)
+ | Iadd (* pop two values, push their sum *)
+ | Isub (* pop two values, push their difference *)
+ | Imul (* pop two values, push their product *)
+ | Ibeq ofs (* pop n2, pop n1, skip ofs forward if n1 = n2 *)
+ | Ibne ofs (* pop n2, pop n1, skip ofs forward if n1 <> n2 *)
+ | Ible ofs (* pop n2, pop n1, skip ofs forward if n1 <= n2 *)
+ | Ibgt ofs (* pop n2, pop n1, skip ofs forward if n1 > n2 *)
+ | Ihalt (* end of program *)
+
+ type code = list instr
+
+ (* Read pointer to code *)
+ inductive codeseq_at code pos code =
+ | codeseq_at_intro : forall c1 c2 c3.
+ codeseq_at (c1 ++ c2 ++ c3) (length c1) c2
+
+
+ lemma codeseq_at_app_right: forall c c1 c2 p.
+ codeseq_at c p (c1 ++ c2) -> codeseq_at c (p + length c1) c2
+
+
+ lemma codeseq_at_app_left: forall c c1 c2 p.
+ codeseq_at c p (c1 ++ c2) -> codeseq_at c p c1
+
+ function push (n:int) (s:stack) : stack = Cons n s
+ function iconst (n:int) : code = Cons (Iconst n) Nil
+ function ivar (x:id) : code = Cons (Ivar x) Nil
+ function isetvar (x:id) : code = Cons (Isetvar x) Nil
+ constant iadd : code = Cons Iadd Nil
+ constant isub : code = Cons Isub Nil
+ constant imul : code = Cons Imul Nil
+ function ibeq (ofs:ofs) : code = Cons (Ibeq ofs) Nil
+ function ible (ofs:ofs) : code = Cons (Ible ofs) Nil
+ function ibne (ofs:ofs) : code = Cons (Ibne ofs) Nil
+ function ibgt (ofs:ofs) : code = Cons (Ibgt ofs) Nil
+ function ibranch (ofs:ofs) : code = Cons (Ibranch ofs) Nil
+ constant ihalt : code = (Cons Ihalt Nil)
+
+ (* The semantics of the virtual machine is given in small-step style,
+ as a transition relation between machine states: triples (program
+ counter, evaluation stack, variable state). The transition relation is
+ parameterized by the code c. There is one transition rule for each
+ kind of instruction, except Ihalt, which has no transition. *)
+
+ inductive transition code machine_state machine_state =
+ | trans_const : forall c p n. codeseq_at c p (iconst n) ->
+ forall s m. transition c (VMS p s m) (VMS (p + 1) (push n s) m)
+
+ | trans_var : forall c p x. codeseq_at c p (ivar x) ->
+ forall s m. transition c (VMS p s m) (VMS (p + 1) (push m[x] s) m)
+
+ | trans_set_var: forall c p x. codeseq_at c p (isetvar x) ->
+ forall n s m. transition c (VMS p (push n s) m) (VMS (p + 1) s m[x<-n])
+
+ | trans_add : forall c p. codeseq_at c p iadd ->
+ forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
+ (VMS (p + 1) (push (n1 + n2) s) m)
+
+ | trans_sub : forall c p. codeseq_at c p isub ->
+ forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
+ (VMS (p + 1) (push (n1 - n2) s) m)
+
+ | trans_mul : forall c p. codeseq_at c p imul ->
+ forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
+ (VMS (p + 1) (push (n1 * n2) s) m)
+
+ | trans_beq: forall c p1 ofs. codeseq_at c p1 (ibeq ofs) ->
+ forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
+ (VMS (if n1 = n2 then p1 + 1 + ofs else p1 + 1) s m)
+
+ | trans_bne: forall c p1 ofs. codeseq_at c p1 (ibne ofs) ->
+ forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
+ (VMS (if n1 = n2 then p1 + 1 else p1 + 1 + ofs) s m)
+
+ | trans_ble: forall c p1 ofs. codeseq_at c p1 (ible ofs) ->
+ forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
+ (VMS (if n1 <= n2 then p1 + 1 + ofs else p1 + 1) s m)
+
+ | trans_bgt: forall c p1 ofs. codeseq_at c p1 (ibgt ofs) ->
+ forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
+ (VMS (if n1 <= n2 then p1 + 1 else p1 + 1 + ofs) s m)
+
+ | trans_branch: forall c p ofs. codeseq_at c p (ibranch ofs) ->
+ forall s m. transition c (VMS p s m) (VMS (p + 1 + ofs) s m)
+
+ (* As usual with small-step semantics, we form sequences of machine
+ transitions to define the behavior of a code. We always start with pc
+ = 0 and an empty evaluation stack. We stop successfully if pc points
+ to an Ihalt instruction and the evaluation stack is empty. *)
+
+ clone export ReflTransClosure with type parameter = code,
+ type state = machine_state, predicate transition = transition
+
+ predicate vm_terminates (c:code) (mi mf:state) =
+ exists p. codeseq_at c p ihalt /\
+ transition_star c (VMS 0 Nil mi) (VMS p Nil mf)
+
+ predicate vm_terminates_non_empty (c:code) (mi mf:state) =
+ exists p s. codeseq_at c p ihalt /\
+ transition_star c (VMS 0 Nil mi) (VMS p s mf)
+
+end
+
+theory Vm_test
+
+ use Vm
+
+ constant m0 : state = (const 0)[Id 1 <- 2]
+ constant c : code = ivar (Id 1) ++ (iconst 1 ++ (iadd ++ ihalt))
+
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ lemma cs_0 : codeseq_at c 0 (ivar (Id 1))
+ lemma cs_1 : codeseq_at c 1 (iconst 1)
+ lemma cs_2 : codeseq_at c 2 iadd
+ lemma cs_3 : codeseq_at c 3 ihalt
+
+ lemma g1 : (* 0 -> 1 *)
+ transition c (VMS 0 Nil m0) (VMS 1 (2 :: Nil) m0)
+
+ lemma g2 : (* 1 -> 2 *)
+ transition c (VMS 1 (2::Nil) m0) (VMS 2 (1::(2 :: Nil)) m0)
+
+ lemma g2_trans : (* 0 -> 2 *)
+ transition_star c (VMS 0 Nil m0) (VMS 2 (1::(2 :: Nil)) m0)
+
+ lemma g3 : (* 2 -> 3 *)
+ transition c (VMS 2 (1::(2::Nil)) m0) (VMS 3 (3::Nil) m0)
+
+ goal g3_trans : (* 0 -> 3 *)
+ transition_star c (VMS 0 Nil m0) (VMS 3 (3::Nil) m0)
+
+ goal g_term :
+ vm_terminates_non_empty c m0 m0
+
+end
+
+
+theory Vm_test2
+
+ use Vm
+
+ constant m0 : state = (const 0)[Id 1 <- 2]
+ constant c : code = ivar (Id 1) ++ (iconst 1 ++ (iadd ++ (isetvar (Id 2) ++ (ihalt))))
+
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ lemma cs_0 : codeseq_at c 0 (ivar (Id 1))
+ lemma cs_1 : codeseq_at c 1 (iconst 1)
+ lemma cs_2 : codeseq_at c 2 iadd
+ lemma cs_3 : codeseq_at c 3 (isetvar (Id 2))
+ lemma cs_4 : codeseq_at c 4 ihalt
+
+ lemma g1 :
+ transition c (VMS 0 Nil m0) (VMS 1 (2 :: Nil) m0)
+
+ lemma g2 :
+ transition c (VMS 1 (2::Nil) m0) (VMS 2 (1::(2 :: Nil)) m0)
+
+ lemma g2_trans :
+ transition_star c (VMS 0 Nil m0) (VMS 2 (1::(2 :: Nil)) m0)
+
+ lemma g3 :
+ transition c (VMS 2 (1::(2::Nil)) m0) (VMS 3 (3::Nil) m0)
+
+ goal g3_trans :
+ transition_star c (VMS 0 Nil m0) (VMS 3 (3::Nil) m0)
+
+ lemma g4 :
+ transition c (VMS 3 (3::Nil) m0) (VMS 4 Nil m0[Id 2<-3])
+
+ goal g4_trans :
+ transition_star c (VMS 0 Nil m0) (VMS 4 Nil m0[Id 2<-3])
+
+ goal g_term :
+ vm_terminates c m0 m0[Id 2<-3]
+
+end
+
+theory Vm_test3
+
+ use Vm
+
+ constant m0 : state = (const 0)[Id 1 <- 2]
+ constant c : code = ibranch 1 ++ (iconst 1 ++ ihalt)
+
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ lemma cs_0 : codeseq_at c 0 (ibranch 1)
+ lemma cs_1 : codeseq_at c 1 (iconst 1)
+ lemma cs_2 : codeseq_at c 2 ihalt
+
+ lemma g1 :
+ transition c (VMS 0 Nil m0) (VMS 2 Nil m0)
+
+ goal g_term :
+ vm_terminates_non_empty c m0 m0
+
+end
+
diff --git a/examples/vm_simple.mlw b/examples/vm_simple.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..d6898b21cb0605d3bee1bb6928c3240761aa2fc1
--- /dev/null
+++ b/examples/vm_simple.mlw
@@ -0,0 +1,95 @@
+theory VM_simple
+
+ use export int.Int
+ use export list.List
+
+ type stack = list int
+
+ type instr =
+ | Iconst int (* push n on stack *)
+ | Iadd (* pop two values, push their sum *)
+ | Isub (* pop two values, push their difference *)
+
+ function pop (st : stack) : (int, stack) =
+ match st with
+ | Nil -> (0, st)
+ | Cons c st' -> (c, st')
+ end
+
+ function push (v : int) (st : stack) : stack = Cons v st
+
+ function fconst (v : int) (st : stack) : stack = push v st
+
+ function fadd (st : stack) : stack =
+ let (a1, st1) = pop st in
+ let (a2, st2) = pop st1 in
+ push (a1 + a2) st2
+
+ function fsub (st : stack) : stack =
+ let (a1, st1) = pop st in
+ let (a2, st2) = pop st1 in
+ push (a2 - a1) st2
+
+end
+
+theory VM_simple_test
+
+ use VM_simple
+
+ goal g1 : (* 1 + 2 = 3 *)
+ fadd (fconst 2 (fconst 1 Nil)) = Cons 3 Nil
+
+ goal g2 : (* 2 - 1 = 1 *)
+ fsub (fconst 1 (fconst 2 Nil)) = Cons 1 Nil
+
+ goal g3 : (* 3 - (1 + 2) = 0 *)
+ fsub (fadd (fconst 2 (fconst 1 (fconst 3 Nil)))) = Cons 0 Nil
+
+ goal g4 : (* (3 - 1) + 2 = 4 *)
+ fadd (fconst 2 (fsub (fconst 1 (fconst 3 Nil)))) = Cons 4 Nil
+
+end
+
+
+theory VM_simple_list
+
+ use export VM_simple
+
+ function vm_i (i : instr) (st : stack) : stack =
+ match i with
+ | Iconst v -> fconst v st
+ | Iadd -> fadd st
+ | Isub -> fsub st
+ end
+
+ function vm (il : list instr) (st : stack) : stack =
+ match il with
+ | Nil -> st
+ | Cons i il' -> vm il' (vm_i i st )
+ end
+
+end
+
+theory VM_simple_list_test
+
+ use VM_simple_list
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ goal g1 : (* 1 + 2 = 3 *)
+ vm (Iconst 1 :: (Iconst 2 :: (Iadd :: Nil))) Nil = 3 :: Nil
+
+ goal g2 : (* 2 - 1 = 1 *)
+ vm (Iconst 2 :: (Iconst 1 :: (Isub :: Nil))) Nil = 1 :: Nil
+
+ goal g3 : (* 3 - (1 + 2) = 0 *)
+ vm (Iconst 3 :: (Iconst 1 :: (Iconst 2 :: (Iadd :: (Isub :: Nil))))) Nil
+ = 0 :: Nil
+
+ goal g4 : (* (3 - 1) + 2 = 4 *)
+ vm (Iconst 3 :: (Iconst 1 :: (Isub :: (Iconst 2 :: (Iadd :: Nil))))) Nil
+ = 4 :: Nil
+
+end
+
+
+
diff --git a/examples/vm_simple/why3session.xml b/examples/vm_simple/why3session.xml
new file mode 100644
index 0000000000000000000000000000000000000000..83ad4d685f4cde2c4f651eead921b1760335720c
--- /dev/null
+++ b/examples/vm_simple/why3session.xml
@@ -0,0 +1,132 @@
+<?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="10" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.7.1" alternative="counterexamples" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Eprover" version="2.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<file name="../vm_ind.mlw" proved="true">
+<theory name="ReflTransClosure" proved="true">
+ <goal name="transition_star_one" proved="true">
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="transition_star_transitive" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="transition_star_transitive.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
+ </goal>
+ <goal name="transition_star_transitive.1" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="VM_ind_test" proved="true">
+ <goal name="c0" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
+ </goal>
+ <goal name="c1" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
+ </goal>
+ <goal name="c2" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
+ </goal>
+ <goal name="c3" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="41"/></proof>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="1"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="55"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="64"/></proof>
+ </goal>
+ <goal name="g3_trans" proved="true">
+ <proof prover="0"><result status="valid" time="0.07" steps="185"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="46"/></proof>
+ </goal>
+</theory>
+</file>
+<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="../vm_mem.mlw" proved="true">
+<theory name="VM_mem_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
+ </goal>
+</theory>
+<theory name="VM_mem_list_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="138"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="137"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../vm_simple.mlw" proved="true">
+<theory name="VM_simple_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="21"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="21"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.02" steps="44"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="31"/></proof>
+ </goal>
+</theory>
+<theory name="VM_simple_list_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.03" steps="113"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.03" steps="113"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.07" steps="224"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.07" steps="227"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/vm_simple/why3session.xml.bak b/examples/vm_simple/why3session.xml.bak
new file mode 100644
index 0000000000000000000000000000000000000000..fd93fcb0c57cb03ec55483fa0b59804a633070b0
--- /dev/null
+++ b/examples/vm_simple/why3session.xml.bak
@@ -0,0 +1,36 @@
+<?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"/>
+<file name="../vm_simple.mlw" proved="true">
+<theory name="VM_simple_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="44"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
+ </goal>
+</theory>
+<theory name="VM_simple_list_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="113"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="113"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="0"><result status="valid" time="0.07" steps="224"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="0"><result status="valid" time="0.07" steps="227"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/vm_simple/why3shapes.gz b/examples/vm_simple/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..7899402116a3e26b0ad9aca419da93ef5386d71e
Binary files /dev/null and b/examples/vm_simple/why3shapes.gz differ
diff --git a/examples/vm_simple/why3shapes.gz.bak b/examples/vm_simple/why3shapes.gz.bak
new file mode 100644
index 0000000000000000000000000000000000000000..1e48fe050851d7d73db8b72fee23aaac8079dfc0
Binary files /dev/null and b/examples/vm_simple/why3shapes.gz.bak differ