Top-level array definition causes runtime failures

[amosr]

Hi,
I came across an example where defining a constant array at the top-level causes a lot of runtime failures, even in functions that do not mention the top-level array. The error is that the logic does not support quantifiers.

type T = enum { A };

const config_const_array: T ^ 1;

node rising_edge(
  i: bool;
) returns (
  b: bool;
)
let
  b = i and (false -> pre (not i));
  --%PROPERTY not b -> true;
tel

I get the following output. I am using an older version, but can reproduce online as well: https://kind.cs.uiowa.edu/app/#temp_35d1ecdf-bca4-46a4-820d-9da0d0cf37d6

$ kind2 bugs/top-array.lus
 kind2 v2.0.0-128-g9ff3188



========================================================================================================================================
Analyzing rising_edge
  with First top: 'rising_edge' (no subsystems)

<Warning> IC3IA disabled: arrays are not supported.

<Error> Runtime failure in 2-induction: SMT solver failed: line 25 column 76: logic does not support quantifiers

<Error> Runtime failure in inductive step: SMT solver failed: line 21 column 76: logic does not support quantifiers

<Error> Runtime failure in property directed reachability (QE): SMT solver failed: line 21 column 76: logic does not support quantifiers

<Error> Runtime failure in bounded model checking: SMT solver failed: line 15 column 76: logic does not support quantifiers

<Error> Caught failure in invariant generator: SMT solver failed: line 20 column 76: logic does not support quantifiers

<Error> Caught failure in invariant generator: SMT solver failed: line 15 column 76: logic does not support quantifiers

<Error> Caught failure in invariant generator: SMT solver failed: line 15 column 76: logic does not support quantifiers

<Error> Caught failure in invariant generator: SMT solver failed: line 15 column 76: logic does not support quantifiers

<Warning> Child process 85397 (2-induction) exited with return code 1

<Warning> Child process 85396 (inductive step) exited with return code 1

<Warning> Terminating useless bounded model checking (PID 85395)

<Warning> Child process 85398 (property directed reachability (QE)) exited with return code 1

<Warning> Terminating useless bounded model checking (PID 85395)

<Warning> Child process 85395 (bounded model checking) exited with return code 1

----------------------------------------------------------------------------------------------------------------------------------------
Summary of properties:
----------------------------------------------------------------------------------------------------------------------------------------
InvProp[l12c3]: unknown
========================================================================================================================================

<Note> Incomplete analysis result: Not all properties could be proven invariant