new Beem aiger models

[Armin Biere]

Jori Dubrovin translated the explicit state model checking
benchmarks from the BEEM benchmark set into our
BTOR format, which were then synthesized to AIGER
with Boolector.

You find all at

http://fmv.jku.at/aiger/#beem

Armin

P.S. We are working on the call for model checkers / benchmarks
for HWMCC'12 and will send it around in a week or two.  This
year is a feature freeze year. So do not expect many changes.

[Armin Biere]

Thanks!

Armin

---------- Forwarded message ----------
From: brayton <bra...@eecs.berkeley.edu>
Date: Tue, Jul 24, 2012 at 7:34 AM
Subject: Re: new Beem aiger models
To: armin...@gmail.com, Armin Biere <bi...@jku.at>


I ran most of the beem examples through super_prove. Attached is an excel spreadsheet of the results. The examples I did not try were some of the 'b' examples since after a while I found that, almost all the time, when the 'b'  version could be solved the 'f' version could be solved as well, but not vice-verse. Time-out was set to 1000 sec.

I thought these results might be useful to others.

Bob

.

[Stefan Kupferschmid]

Hi all,

first of all I would like to thank Bob for sending around the results of the beem benchmarks. I just had a look at the table and discovered the following:

1. Some entries are doubled:

- beembrptwo2f3
- beemextnc4f1

2. There are some benchmarks that do not come with the beemaigs.7z archive:

- beemcoll6f1_best
- beemcoll6f1_best_aig
- beemcoll6f1_rpm
- beemcoll6f1_savetemp
- beemcoll6f1_savetempreal
- beemcoll6f1_smp

3. Benchmark beemldelec1f1 from the beemaigs.7z archive does not appear in the table

As I am always interested in new benchmarks I would like to ask Bob whether it is possible to make beemcoll6f1_best - beemcoll6f1_smp available.

Kindest regards,
   Stefan

[brayton]

Stefan,

Good eye!

Here is the corrected table.

The duplicated have been removed,

The files with additional extensions like "best" were generated djuring a run of super_prove and are temporary intermediate files. They should not have been there. I removed them.

I must have inadvertently deleted the result for beemldelec1f1 and it is put back in.

Bob