[SMT-LIB] Bug in pattern in smtlib2 benchmarks

[Jochen Hoenicke]

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