Array length

[hal...@seas.upenn.edu]

Thanks for making a really great solver - I've used boolector for one application so far (bit-vectors only) and see great improvements over z3!

I'd like to use boolector for another application involving arrays.  The only problem is that I need to upper and lower bound the array length.  Is there any way to do that using boolector?

[Mathias Preiner]

Hi!

What you could try is to either change the bit-width of the index type
of the array (if the upper bound is a power of two) or to add
constraints for each index that ensures that the index is between an
upper and lower bound.

Mathias

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To post to this group, send email to bool...@googlegroups.com
> <mailto:bool...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/boolector.
> For more options, visit https://groups.google.com/d/optout.