CVC4 memlimit registered as high failure
I found that if cvc4 hits the memory limit, why3 registers this as a HighFailure instead of an OutOfMemory result. I found that the fixes on !530 (merged) don't address the issue on my side, and based on my investigations, I don't see how they could.
Basically, it seems that cause is that Call_Provers.analyze_result
is called with a kind of default exit result, based on the exit code of the process (see Call_provers.parse_prover_run
). If signaled
is true this default exit result is HighFailure. analyze_result
basically always uses this default exit result unless the computed result is Valid
. This is because the local analyse
function, which recursively goes through the various bits of parsed prover output, always uses the last Answer.
The following patch changes analyse
to instead use the first encountered answer (unless the answer is valid). Should I propose a merge request?
diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml
index 041c46dbb..ca6bc2fae 100644
--- a/src/driver/call_provers.ml
+++ b/src/driver/call_provers.ml
@@ -266,12 +266,12 @@ let analyse_result exit_result res_parser printer_mapping out =
let m = res_parser.prp_model_parser printer_mapping model_str in
Debug.dprintf debug "Call_provers: model:@.";
debug_print_model ~print_attrs:false m;
- analyse ((res, m) :: saved_models) (Some res) tl
+ analyse ((res, m) :: saved_models) (if saved_res = None then Some res else saved_res) tl
| Answer res :: tl ->
if res = Valid then
(Valid, [])
else
- analyse saved_models (Some res) tl
+ analyse saved_models (if saved_res = None then Some res else saved_res) tl
| Model _fail :: tl -> analyse saved_models saved_res tl
in