From 680be27a954886890add7c260a2b998061029ce8 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Sat, 28 Mar 2015 07:03:42 +0100
Subject: [PATCH] update proofs by veriT

---
 examples/logic/einstein/why3session.xml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/examples/logic/einstein/why3session.xml b/examples/logic/einstein/why3session.xml
index e1fec3eb9..ee0593461 100644
--- a/examples/logic/einstein/why3session.xml
+++ b/examples/logic/einstein/why3session.xml
@@ -14,10 +14,10 @@
 <prover id="9" name="Z3" version="3.2" timelimit="30" memlimit="1000"/>
 <prover id="10" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
 <prover id="11" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="1000"/>
-<prover id="12" name="veriT" version="201310" timelimit="5" memlimit="4000"/>
 <prover id="13" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
 <prover id="14" name="Vampire" version="0.6" timelimit="20" memlimit="1000"/>
 <prover id="15" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
+<prover id="16" name="veriT" version="201410" timelimit="5" memlimit="1000"/>
 <file name="../einstein.why" expanded="true">
 <theory name="Bijection" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
 </theory>
@@ -36,10 +36,10 @@
  <proof prover="9"><result status="valid" time="0.26"/></proof>
  <proof prover="10"><result status="valid" time="2.88"/></proof>
  <proof prover="11"><result status="valid" time="12.38" steps="969"/></proof>
- <proof prover="12"><result status="valid" time="0.02"/></proof>
  <proof prover="13"><result status="unknown" time="0.06"/></proof>
  <proof prover="14"><result status="valid" time="1.50"/></proof>
  <proof prover="15"><result status="valid" time="2.86" steps="642"/></proof>
+ <proof prover="16"><result status="timeout" time="4.99"/></proof>
  </goal>
  <goal name="Wrong" expanded="true">
  <proof prover="0"><result status="unknown" time="15.98"/></proof>
@@ -54,10 +54,10 @@
  <proof prover="9" timelimit="5"><result status="timeout" time="4.96"/></proof>
  <proof prover="10"><result status="timeout" time="5.00"/></proof>
  <proof prover="11"><result status="unknown" time="9.98"/></proof>
- <proof prover="12"><result status="timeout" time="4.97"/></proof>
  <proof prover="13"><result status="unknown" time="0.06"/></proof>
  <proof prover="14" timelimit="5"><result status="timeout" time="10.08"/></proof>
  <proof prover="15"><result status="unknown" time="1.33"/></proof>
+ <proof prover="16"><result status="timeout" time="4.98"/></proof>
  </goal>
  <goal name="G2" expanded="true">
  <proof prover="0"><result status="valid" time="12.12" steps="1747"/></proof>
@@ -72,10 +72,10 @@
  <proof prover="9"><result status="valid" time="0.62"/></proof>
  <proof prover="10"><result status="valid" time="0.79"/></proof>
  <proof prover="11"><result status="valid" time="7.55" steps="1007"/></proof>
- <proof prover="12"><result status="valid" time="0.02"/></proof>
  <proof prover="13" timelimit="3"><result status="unknown" time="0.06"/></proof>
  <proof prover="14"><result status="valid" time="1.27"/></proof>
  <proof prover="15"><result status="valid" time="1.82" steps="523"/></proof>
+ <proof prover="16"><result status="timeout" time="4.99"/></proof>
  </goal>
 </theory>
 </file>
-- 
GitLab