projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f6215a3) | patch
Avoid tokenizing FP tokens in non-FP input
authorAndres Noetzli <noetzli@stanford.edu>
Tue, 16 May 2017 18:33:38 +0000 (11:33 -0700)
committerAndres Noetzli <noetzli@stanford.edu>
Tue, 16 May 2017 18:33:38 +0000 (11:33 -0700)
commit9ef270c5853b629a6f883b0b601cc7188b58cc0a
treec0ac83f78f5be7a45f8406ad37bad56da51c1112tree
parentf6215a3d10c11976cffbeb4c88223e8434ffc4d3commit | diff
Avoid tokenizing FP tokens in non-FP input

This commit addresses bug 807. CVC4 was parsing floating-point related tokens
such as NaN as floating-point tokens even for inputs that do not use the FP
theory, which lead to failing SMT-LIB benchmarks that declare functions named
NaN.
src/parser/smt2/Smt2.g diff | blob | history