Type inference check reports error when using integer value for time expression

ultimate-pa / hanfor

Hanfor helps analyzing and formalizing requirements.

https://ultimate-pa.github.io/hanfor/

GNU Lesser General Public License v3.0

9 stars 3 forks source link

Closed henkele closed 2 years ago

henkele commented 2 years ago

Steps to reproduce:

Add the formalization:
Globally, it is always the case that "true" holds at least every "3" time units.
Requirement is tagged with 'Type_inference_error' tag and the following description: - Types inconsistent: 3 had Type BoogieType.error inferred as BoogieType.int