Hi, Aaron Bradley (Stanford) submitted several benchmarks for QF_AUFLIA and AUFLIA. The benchmarks were produced using his tool: piVC. We've also posted some benchmarks (AUFLIA) from the haRVey theorem prover. The new benchmarks can be downloaded at: http://www.csl.sri.com/users/demoura/smt-comp/benchmarks.shtml Leonardo