LLREVE Examples

• Files with extension .smt2 are in SMT-LIB format.
  • Files with extension .smt2 (directory quant) that operate on heaps use universally quantified predicates
  • Files with extension .array.smt2 (directory arrays) that operate on heaps use arrays as predicate arguments.
• Files with extension .muz are in Z3 rules format (they take arrays as predicate arguments)

Contributing email

To: arie.gurfinkel
From: Mattias Ulbrich

Hi Arie,

there was a recently introduced problem with the smt generation. I hope I fixed that and can send you now .smt2 and .muz examples from llreve.

The ones named "faulty_" are not supposed to have a solution.

The others tend to work on one of the engines we tried them on: eldarica, z3-spacer, z3-pdr or z3-duality.

I will come up with a few examples which would be nice but seem not in reach at the moment.

Best regards, Mattias

Contributor

Mattias Ulbrich