diff options
| author | Frédéric Besson | 2020-08-10 16:45:35 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2020-08-10 18:55:25 +0200 |
| commit | 74932ad2ff431f49370d8bb0f730a588b192b484 (patch) | |
| tree | bfd25ebb404a583512785a54854dcaa5440c2b5f /kernel/genOpcodeFiles.ml | |
| parent | ef08abec26c2f0017d1136870f8f99144e579538 (diff) | |
[micromega] Fix bug#12790
zify used to generate many syntactic positivity constraints when translating a goal
from nat to Z. For instance, to state that the product of 2 integers
is positive. Instead, lia performs an interval analysis that is more semantic.
The bug was that the interval analysis was performed after the
elimination of equations. The current workaround is to perform
interval analysis before and after eliminating equations.
bla
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions