ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

examples: reconstruct sessions

Browse Source 
still problematic:

  tests-provers/div
  tests-provers/div_real
  check-builtin/int
  bts/fsetint
  logic/bitvectors
  logic/einstein
  logic/genealogy
  bitvectors/power2
  bellman_ford
  knuth_prime_numbers
  vstte12_combinators
  hoare_logic/blocking_semantics5

known issues:
- Timeout is not always recognized
- why3 tactic does not work: ENOENT on connect()
- temporary output files are created in the curdir
- temporary output files are sometimes not erased
- socket file is created in the curdir
This commit is contained in:
Andrei Paskevich
2016-04-14 23:19:42 +02:00
parent b92e8a7df8
commit 0f9ded381b
201 changed files with 4923 additions and 4923 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
examples/decrease1/why3session.xml
View File

@@ -2,18 +2,18 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="10" memlimit="0"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="5" name="CVC3" version="2.2" timelimit="10" memlimit="0"/>
<prover id="6" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="7" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="5" name="CVC3" version="2.2" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="6" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../decrease1.mlw" expanded="true">
<theory name="Decrease1" sum="7c49cfeea622335075ec3d6212620b2b" expanded="true">
<goal name="decrease1_induction" expanded="true">
<proof prover="3" edited="decrease1_Decrease1_decrease1_induction_2.v"><result status="valid" time="1.10"/></proof>
<proof prover="3" edited="decrease1_Decrease1_decrease1_induction_2.v"><result status="valid" time="0.82"/></proof>
</goal>
<goal name="WP_parameter search" expl="VC for search" expanded="true">
<transf name="split_goal_wp" expanded="true">