[SMT-LIB] Bug in pattern in smtlib2 benchmarks

[Morgan Deters]

Hi Jochen,

Thanks for catching this.  After reading what the spec says about
:pattern's intended use, this does look like an error to me.  I'll
correct the translator.

Morgan


On Mon, Feb 21, 2011 at 10:07 AM, Jochen Hoenicke
<hoenicke at informatik.uni-freiburg.de> wrote:
> Hello,
>
> we started implementing pattern-based quantifier instantiation in our
> solver and stumbled over something that looks like a bug in the
> benchmark converter.
>
> The file AUFLIA/boogie/AdditiveMethods_AdditiveMethods.N.smt2 contains the line
>
> (assert (forall ((?A Int) (?r Int) (?T Int)) (! (let ((?v_0
> (ValueArray ?A ?r))) (=> (subtypes ?T ?v_0) (= ?T ?v_0))) :pattern
> ((subtypes ?T ?v_0)) )))
>
> Note that in this construct the annotation ":pattern ((subtypes ?T
> ?v_0))" is outside of the scope of the let command, hence the variable
> ?v_0 is undefined in this pattern.
>
> Interestingly, the corresponding assumption in smtlib-1.2 does not
> contain the let at all:
>
> :assumption
>  (forall (?A Int) (?r Int) (?T Int)
>   (implies (subtypes ?T (ValueArray ?A ?r)) (= ?T (ValueArray ?A ?r)))
>   :pat {(subtypes ?T (ValueArray ?A ?r))})
>
> Regards,
>  Jochen
>
> --
> Jochen Hoenicke,
> Email: hoenicke at informatik.uni-freiburg.de  Tel: +49 761 203 8243
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>



-- 
Morgan Deters
mdeters at gmail.com