Allow (_ to_fp ...) in strict parsing mode (#2566)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 3 Oct 2018 01:10:54 +0000 (18:10 -0700)
committerAina Niemetz <aina.niemetz@gmail.com>
Wed, 3 Oct 2018 01:10:54 +0000 (18:10 -0700)
commitc48dd01b92f4704c99ca6833b94759dee42106a8
tree3dcf129eb8c022c0538924ad988285e825fd48ec
parent457a5000f46cfd7ce58525b75930b87e8572c94f
Allow (_ to_fp ...) in strict parsing mode (#2566)

When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
src/parser/smt2/smt2.cpp
test/regress/CMakeLists.txt
test/regress/Makefile.tests
test/regress/regress0/parser/to_fp.smt2 [new file with mode: 0644]