Commit 34e16135 authored by MARCHE Claude's avatar MARCHE Claude

CVC4: there is no specific output message for stepslimitreached

parent 41b1edfb
......@@ -40,8 +40,10 @@ transformation "encoding_smt_if_poly"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
(** Extra theories supported by CVC4 *)
......
......@@ -51,8 +51,10 @@ transformation "encoding_smt_if_poly"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
(** Extra theories supported by CVC4 *)
......
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