Segfault with Bitvector Arrays

[evanlohn]

In commit 3130e49 on Amazon Linux compiled with gcc-7.3.1, declaring an array and then defining a function with a quantifier results in a segfault, even when the function does not use the array. Example below:

(declare-const s (Array (_ BitVec 8) (_ BitVec 8)))
(define-fun f 
  ((a (_ BitVec 8)))
  Bool
  (forall ((j (_ BitVec 8))) (bvult (_ bv0 8) a)))

(assert (f (_ bv0 8)))
(check-sat)

In debug mode, this gives

Assertion failed: (free_vars.size() > 0), function compute_variable_dependencies, file bzlaslvquant.cpp, line 2052.
[bitwuzla>main] CAUGHT SIGNAL 6
unknown
Abort

Removing the forall or the declaration of s gets rid of the segfault. I have also run into segfaults using Array constants in function bodies, but I'm hoping fixing this will fix that problem as well since the same assertion fails in debug mode.

[evanlohn]

Oops, this was meant for Bitwuzla