[SMT-LIB] Will Smtlib support sequences?

[Laar, P.J.L.J. (Pierre) van de]

Dear Smtlib developers,

With the current version of smtlib, I have problems modelling arrays in programming languages that have a finite size,
since Arrays in smtlib have infinite size.
Recently, I discovered that Z3 supports exactly what I need: Sequences
(see e.g. http://rise4fun.com/Z3/tutorial/sequences).
Will smtlib also support Sequences soon?
To be more precise: Will Sequences be incorporated in version 2.6, 3.0, or even later?

Thanks for your attention.

Pierre van de Laar
[TNO-ESI_logo-email-signature]



Dr. Piërre van de Laar
Research Fellow





Embedded Systems Innovation by TNO
De Rondom 1, 5612 AP Eindhoven
Postbus 6235, 5600 HE  Eindhoven
The Netherlands

T   +31 8886 69388
E   pierre.vandelaar at tno.nl<mailto:pierre.vandelaar at tno.nl>
W www.esi.nl<http://www.esi.nl/>

TNO Eindhoven<http://www.tno.nl/locaties/eh>
Disclaimer<http://www.tno.nl/emaildisclaimer>



This message may contain information that is not intended for you. If you are not the addressee or if this message was sent to you by mistake, you are requested to inform the sender and delete the message. TNO accepts no liability for the content of this e-mail, for the manner in which you use it and for damage of any kind resulting from the risks inherent to the electronic transmission of messages.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image001.png
Type: image/png
Size: 9674 bytes
Desc: image001.png
URL: </pipermail/smt-lib/attachments/20160509/22d522a0/attachment-0001.png>