Commit 45892471 authored by David Hauzar's avatar David Hauzar

Bugfix: counter-example model is printed if it is not empty.

parent 34f1ba18
......@@ -135,7 +135,7 @@ let print_steps fmt s =
let print_prover_result fmt
{pr_answer=ans; pr_status=status; pr_output=out; pr_time=t; pr_steps=s; pr_model=m} =
fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
if Model_parser.is_model_empty m then begin
if not (Model_parser.is_model_empty m) then begin
fprintf fmt "\nCounter-example model:";
Model_parser.print_model fmt m
end;
......
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