[SMT-LIB] New SMT-LIB release for SMT-COMP 2011---includes fixes, additions

[Tjark Weber]

Morgan,

On Mon, 2011-05-16 at 00:25 -0400, Morgan Deters wrote:
> Apologies if I have forgotten to acknowledge anyone.  Please let me
> know if there are any benchmark compliance issues, or if I have
> neglected to include a fix, or a benchmark contribution, in this
> release.

Benchmark QF_BV/mcm/01.smt2 (previously QF_NIA/mcm/01.smt2) contains a
definition

  (define-fun shlok ((x (_ BitVec 11)) (y (_ BitVec 11))) Bool
    (= (bvand x (mask1 y)) (_ bv0 12)))

(line 52f.).  Here the first argument to =, (bvand x (mask1 y)), is of
sort (_ BitVec 11), while the second argument, (_ bv0 12), is of sort
(_ BitVec 12).  Therefore, I believe the term is ill-typed (unless, of
course, I am overlooking some implicit conversion).

Numerous other benchmarks in the mcm family are also affected.

Kind regards,
Tjark