Commit 2d0cbd7b authored by MARCHE Claude's avatar MARCHE Claude

Improved regexps for "outofmemory" result

parent 96c5d906
......@@ -9,6 +9,7 @@ valid "Valid"
invalid "Invalid"
unknown "I don't know" ""
timeout "Timeout"
outofmemory "Fatal error: out of memory"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s)"
time "why3cpulimit time : %s s"
......
......@@ -9,7 +9,7 @@ filename "%f-%t-%g.cvc"
fail "Parse Error: \\(.*\\)" "\\1"
valid "Valid\\."
unknown "Unknown\\." ""
outofmemory "Out of memory\\|std::bad_alloc"
outofmemory "Out of memory\\|std::bad_alloc\\|GNU MP: Cannot allocate memory"
time "why3cpulimit time : %s s"
(* À discuter *)
......
......@@ -8,7 +8,7 @@ filename "%f-%t-%g.smt"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
outofmemory "(error \"out of memory\")\\|Cannot allocate memory"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
time "why3cpulimit time : %s s"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="verifythis_PrefixSumRec/why3session.xml" shape_version="2">
<prover
......@@ -21,7 +21,7 @@
<prover
id="4"
name="Coq"
version="8.3pl3"/>
version="8.3pl4"/>
<prover
id="5"
name="Z3"
......@@ -109,7 +109,7 @@
edited="PrefixSumRec_PrefixSumRec_phase1_frame_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.44"/>
<result status="valid" time="0.76"/>
</proof>
</goal>
<goal
......@@ -127,7 +127,7 @@
edited="PrefixSumRec_PrefixSumRec_phase1_frame2_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.44"/>
<result status="valid" time="0.75"/>
</proof>
</goal>
<goal
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment