projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 36bb555) | patch
Properly parse numerals as real when integers are disabled (#8591)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 8 Apr 2022 20:38:52 +0000 (15:38 -0500)
committerGitHub <noreply@github.com>
Fri, 8 Apr 2022 20:38:52 +0000 (13:38 -0700)
commit80959b3c2c4ace7a7a06b996418776b554e3f184
tree6e64b2a31484f8354e68ab204b55c93fe8d52ccctree
parent36bb555ad804416f74fb582042d2999b216c51e0commit | diff
Properly parse numerals as real when integers are disabled (#8591)

SMT-LIB says numerals are real when integers are not included in the logic.

Due to subtyping, we don't complain internally, although if subtyping is eliminated, this fix is necessary.
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history