diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-12-15 11:03:26 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-12-15 13:24:34 -0800 |
| commit | 577d4b6bde6c31bd77254de9355666f6b698cc45 (patch) | |
| tree | 5ad6b0e9f0e0ec8fb98018d5415c698de82c284c /src/options/quantifiers_options.toml | |
| parent | effb0d47ba5bfaebae17dcd06153489dccd90eff (diff) | |
Explicitly disallow `mkConst(Rational)`
The `Rational` payload can be associated with two kinds (`CONST_INTEGER`
and `CONST_RATIONAL`), so we should never call
`NodeManager::mkConst(Rational)`, but instead use
`NodeManager::mkConstInt()` and `NodeManager::mkConstReal()`. Currently,
calling `NodeManager::mkConst(Rational)` silently creates an integer
constant, which is dangerous. This commit makes it a compile-time error
instead.
Diffstat (limited to 'src/options/quantifiers_options.toml')
0 files changed, 0 insertions, 0 deletions