Commit ffe1235d authored by MARCHE Claude's avatar MARCHE Claude

no 'Unknown: Unknown' prover result anymore

parent 15515d3e
......@@ -7,7 +7,7 @@ filename "%f-%t-%g.why"
valid "Valid"
invalid "Invalid"
unknown "I don't know" "Unknown"
unknown "I don't know" ""
timeout "Timeout"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s)"
......
......@@ -6,7 +6,7 @@ printer "smtv2"
filename "%f-%t-%g.smt2"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
time "why3cpulimit time : %s s"
(*transformation "simplify_recursive_definition"*)
......
......@@ -7,7 +7,7 @@ printer "gappa"
filename "%f-%t-%g.gappa"
valid 0
unknown "no contradiction was found\\|some enclosures were not satisfied" "Unknown"
unknown "no contradiction was found\\|some enclosures were not satisfied" ""
time "why3cpulimit time : %s s"
fail "Error: \\(.*\\)" "\\1"
......
......@@ -6,7 +6,7 @@ printer "simplify"
filename "%f-%t-%g.sx"
valid "\\bValid\\b"
unknown "\\bInvalid\\b" "Unknown"
unknown "\\bInvalid\\b" ""
time "why3cpulimit time : %s s"
(*transformation "simplify_recursive_definition"*)
......
......@@ -10,7 +10,7 @@ timeout "Ran out of time"
(* timeout "Resource limit exceeded" *)
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" "Unknown"
unknown "No Proof Found" ""
fail "Failure.*" "\"\\0\""
time "why3cpulimit time : %s s"
(* time "%h:%m:%s on the problem" *)
......
......@@ -6,13 +6,13 @@ filename "%f-%t-%g.p"
valid "Refutation found"
(* timeout "Aborted by signal SIGXCPU on" *)
unknown "Time limit reached" "Time out"
unknown "Refutation not found" "Unknown"
unknown "Refutation not found" ""
outofmemory "Memory limit exceeded"
(* invalid "Completion found" *)
(* invalid "SZS status CounterSatisfiable" *)
(* timeout "Ran out of time" *)
(* timeout "Resource limit exceeded" *)
(* unknown "No Proof Found" "Unknown" *)
(* unknown "No Proof Found" "" *)
(* fail "Failure.*" "\"\\0\"" *)
time "why3cpulimit time : %s s"
(* time "%h:%m:%s on the problem" *)
......
......@@ -6,7 +6,7 @@ printer "smtv1"
filename "%f-%t-%g.smt"
valid "^unsat"
unknown "^\\(unknown\\|sat\\)" "Unknown"
unknown "^\\(unknown\\|sat\\)" ""
time "why3cpulimit time : %s s"
(* À discuter *)
......
......@@ -6,7 +6,8 @@ printer "yices"
filename "%f-%t-%g.ycs"
valid "\\bunsat\\b"
unknown "\\bunknown\\b\\|\\bsat\\b\\|feature not supported: non linear problem" "Unknown"
unknown "\\bunknown\\b\\|\\bsat\\b" ""
unknown "feature not supported: non linear problem" "non linear arith"
time "why3cpulimit time : %s s"
(* À discuter *)
......
......@@ -7,7 +7,7 @@ printer "smtv2"
filename "%f-%t-%g.smt"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
outofmemory "(error \"out of memory\")\\|Cannot allocate memory"
time "why3cpulimit time : %s s"
......
......@@ -6,7 +6,7 @@ printer "smtv1"
filename "%f-%t-%g.smt"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
time "why3cpulimit time : %s s"
......
......@@ -92,8 +92,8 @@ let print_prover_answer fmt = function
| OutOfMemory -> fprintf fmt "Ouf Of Memory"
| Unknown "" -> fprintf fmt "Unknown"
| Failure "" -> fprintf fmt "Failure"
| Unknown s -> fprintf fmt "Unknown: %s" s
| Failure s -> fprintf fmt "Failure: %s" s
| Unknown s -> fprintf fmt "Unknown (%s)" s
| Failure s -> fprintf fmt "Failure (%s)" s
| HighFailure -> fprintf fmt "HighFailure"
let print_prover_status fmt = function
......
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