diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-10-28 04:01:28 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-10-28 04:01:28 -0700 |
| commit | bab652d9fa2b2efac07b3b686cff3f67b5ef5fda (patch) | |
| tree | a46e22bfa4d068b7f241bf86e06846450d7b699d /NEWS | |
| parent | 46f5a39730ebd42421963c23de81a75652fb6629 (diff) | |
[FP] Fix overly restrictive assertionprojIssue327
Fixes https://github.com/cvc5/cvc5-projects/issues/327. When generating
refinement lemmas, we were asserting that the concrete value of
conversion from real to a floating-point number was either normal or
subnormal. However, it can also be zero. This commit fixes the assertion
and adds a modified version of the regression that triggers the same
error and terminates quickly with the fix.
Diffstat (limited to 'NEWS')
0 files changed, 0 insertions, 0 deletions