projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5f8b41a) | patch
Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),
authorMorgan Deters <mdeters@gmail.com>
Thu, 30 Jun 2011 21:03:52 +0000 (21:03 +0000)
committerMorgan Deters <mdeters@gmail.com>
Thu, 30 Jun 2011 21:03:52 +0000 (21:03 +0000)
commitaf25c3f8498198dd6dd114c3b4ef39af54611e1e
tree6f0f8e84685bf58dcd003e9f3da630e58163873etree
parent5f8b41a0b896c2224ac4fc3b13eba7c370764df6commit | diff
Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),
when --strict-parsing is off (which it is by default).  The danoint benchmarks
have such monsters.
src/parser/smt/Smt.g diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history