smtlib2 parsing bug

[Edward Schwartz]

Hi,

I think stp has a bug when parsing let expressions in smtlib2
benchmarks. Here is a triggering test input:

(set-logic QF_ABV)
(set-info :smt-lib-version 2.0)

(assert (let ((?foo (let ((?foo2 (_ bv1 1))) ?foo2))) (= ?foo (_ bv1 1))))
(check-sat)
(exit)

In smtlib1, let x = e in <term> is not allowed. It is allowed in
smtlib2, however. It looks like stp's smtlib2 parser was derived from
the smtlib1 parser, and inherited the wrong policy.

I am attaching a patch that changes the parser. It seems to work, but
I put little effort into making sure it is the right way to fix it.

Thanks,

Ed

[Ryan Govostes]

It doesn't look like this has yet been checked in. Is anyone reviewing patches on this list?