summaryrefslogtreecommitdiff
path: root/src/theory/substitutions.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2011-06-30 21:03:52 +0000
committerMorgan Deters <mdeters@gmail.com>2011-06-30 21:03:52 +0000
commitaf25c3f8498198dd6dd114c3b4ef39af54611e1e (patch)
tree6f0f8e84685bf58dcd003e9f3da630e58163873e /src/theory/substitutions.h
parent5f8b41a0b896c2224ac4fc3b13eba7c370764df6 (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.
Diffstat (limited to 'src/theory/substitutions.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback