[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Matthias Heizmann]

Hi all,

I also want to submit QF_FPBV and QF_FPABV (and probably even a few FPBV and 
FPABV) benchmarks that were produced by our Ultimate Automizer tool.


Currently, I have two problems.

1. I produced around 30000 benchmarks. Most of them are trivial, but there are 
at least a few hundred interesting ones.
All our benchmarks first declare a lot of function symbols that are never used. 
If I could remove all the unused functions, I would be able to filter the 
trivial ones.
How do you remove the unused function symbol declarations?

2. Our arrays have the following sort.
    (Array (_ BitVec 32) (Array (_ BitVec 32) (_ BitVec 8)))
Reason: Our tool models the heap of a C program (unsoundly) via a two 
dimensional array. The array indices represent the pointer, the array value 
represents the byte that is stored at that address. We convert floats to 
bitvectors and store them bytewise.
So far we always failed to submit our array benchmarks because the logics do 
not allow nested array sorts, e.g., QF_ABV only allows 
(Array (_ BitVec i) (_ BitVec j)).

We would appreciate very much if QF_FPABV would also allow the following sort.
    (Array (_ BitVec 32) (Array (_ BitVec 32) (_ BitVec 8)))

Best,
Matthias
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part.
URL: </pipermail/smt-comp/attachments/20170423/44bef880/attachment.asc>