add warning if fv finds an invalidating model and decimals use 255

[rsoeldner]

Addresses #1107 by adding a warning in case, an invalidating model is found which uses 255 decimal places. This indicates a precision underflow.

The following program

(module test GOVERNANCE
  (defcap GOVERNANCE() true)
  
  (defun get-refund:decimal (balance:decimal stakers:integer)
    @model [ (property  (> result 0.0))  ]
    
    (enforce (> balance 0.0) "balance must be non-negative")
    (enforce (> stakers 0) "stakers must be non-negative")

    (/ balance stakers)) )

(verify 'test)

will result in this output:

The warning is placed in the corresponding FV trace.