stp/stp — pull request #58 by edmcman (2013-10-11 17:59:33+00:00)
Title: Smtlib2 parser does not parse Let correctly

See https://gist.github.com/edmcman/6938918#file-example1-smt2

ed@ed-Ubu64 /tmp$ cvc3 -lang smt2 example1.smt2
sat
ed@ed-Ubu64 /tmp$ z3 -smt2 example1.smt2
sat
ed@ed-Ubu64 /tmp$ boolector --smt2 example1.smt2
sat
ed@ed-Ubu64 /tmp$ ~/f13/stp/build/stp --SMTLIB2 example1.smt2
syntax error: line 7
syntax error, unexpected LET_TOK
token: let
Fatal Error:

The problem is that a term is bound inside of a formula. https://github.com/stp/stp/pull/9 was supposed to fix this, but it was apparently incomplete. I have spent more time looking at the smtlib2 parser, and I believe this is the correct way to fix it.