[SMT-COMP] Unsat core track - examples?

[Matthias Heizmann]

Hi Guy,

Sorry, I forgot the third step in our pre-processing.

3. We replace each (assert fmla) by
    (assert (! fmla) :named freshId)
where "freshId" is some identifier that does not occur elsewhere in the script.

Best,
Matthias


On Saturday, May 28, 2016 01:24:23 Matthias Heizmann wrote:
> Hi Guy,
> 
> there will be no special benchmarks for the unsat core track. We will take
> benchmarks from the Main Track whose result is "unsat" and pre-process them
> as follows.
> 1. We prepend the command
>     (set-option :produce-unsat-cores true)
> 2. We add the
>     (get-unsat-core)
> command directly after the check-sat.
> 
> Best,
> Matthias
> 
> On Friday, May 27, 2016 16:13:10 Guy Katz wrote:
> > Hello,
> > Are there any benchmark examples available for the unsat core track?
> > 
> > Regards,
> > Guy
> > _______________________________________________
> > SMT-COMP mailing list
> > SMT-COMP at cs.nyu.edu
> > http://cs.nyu.edu/mailman/listinfo/smt-comp
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part.
URL: </pipermail/smt-comp/attachments/20160528/3e3977cf/attachment.asc>