Check that no answers are lost by Call_prover.analyse_result
In Call_prover.analyse_result
, the code recursively goes through the output of the prover, checking if some regexp are matched e.g. for outofmemory or timeout errors.
In the case | Answer res1 :: (Answer res2 :: tl as tl1)
, there is a specific treatment for Unknown
answers, but the default case simply ignores the answers res1
and res2
when calling recursively analyse saved_models saved_res tl1
.