Commit d25dbe07 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Change message when no counterexamples were generated.

parent 916af21b
......@@ -922,7 +922,10 @@ end
Pp.string_of (Model_parser.print_model_human ?me_name_trans:None)
res.Call_provers.pr_model
in
result ^ "\n\n" ^ "Counterexample suggested by the prover:\n\n" ^ ce_result
if ce_result = "" then
result ^ "\n\n" ^ "The prover did not return counterexamples."
else
result ^ "\n\n" ^ "Counterexample suggested by the prover:\n\n" ^ ce_result
| None -> "Result of the prover not available.\n"
in
P.notify (Task (nid, prover_text ^ prover_ce, list_loc))
......
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