diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-10 15:18:13 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-10 15:18:13 -0800 |
| commit | 51d2682c44761e0b3a30e75188b390b791d5dd48 (patch) | |
| tree | 0d1471f26ad931803ed4849981b972011ac84d5b /src/theory/quantifiers/quantifiers_rewriter.cpp | |
| parent | 82fa0b8a67d076287cc4c4105a42fcabc459fd18 (diff) | |
Removed division by constant handling for CBQI BV (unsound). (#1508)
This removes division by constant handling in the BV inverter introduced in #1498.
Division by constant was simplified to:
x / s OP t ---> x = t / s^-1 if s odd and there exists a multiplicative modular inverse s^-1.
This however, is incorrect since
x / s * 1 / s^-1 != x / (s * s^-1)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
0 files changed, 0 insertions, 0 deletions