kind2-mc/kind2

Error with inductive definition of bounded arrays of records

Closed this issue · 1 comments

type rational = { n: int; d: int };

node Test () returns ()
var rats: rational^4;
let 
    rats[i] = if i = 0 then rational { n = 0 ; d = 1} else rational { n = rats[i-1].n ; d = 1};
tel

Produces the error in kind2 v1.9.0:

Type mismatch in equation: record indexes do not match 
Source: parse

This also fails with the same error:
rats[i] = rational { n = 0 ; d = 1} ;

I'm not sure if I am doing something unsupported. The user doc states that kind2 supports arrays of records.

Thank you for reporting this bug. It is a bug in the new front-end introduced in v1.6.0. As a temporary workaround, you can enable the old front-end by passing --old_frontend true to Kind 2.

Support for arrays is an experimental feature. We are considering dropping its support and replacing arrays with other high-level data structures like maps. We would appreciate it if you could provide feedback on how you use arrays and what for.

Thank you!