FV: Direct verification failure indication

[EnoF]

Is your enhancement request related to a problem? Please describe.

When a invalidating model has been found, we print the path it took to reach that invalidating model, but we do not have any reporting on which model property has been invalidated.

Describe the solution you'd like

When verifying this:

(module test G
  (defcap G() true)

  (defcap ONE (i:integer)
    (enforce (= i 1) "Needs 1")
  )

  (defun test(i:integer)
    @model [
      (property (= i 1))
    ]
    (require-capability (ONE i))
    i
  )
)

(verify 'test)

I'd like to see:

OutputFailure: Invalidating model found in test.test
  Program trace:
    entering function test.test with argument
      i = 0

      returning with 0

  Property (= i 1) has been invalidated

Load successful

Currently it reports this:

OutputFailure: Invalidating model found in test.test
  Program trace:
    entering function test.test with argument
      i = 0

      returning with 0

Load successful