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 | |
| 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
| -rw-r--r-- | plugins/micromega/certificate.ml | 5 | ||||
| -rw-r--r-- | test-suite/micromega/bug_12790.v | 8 |
2 files changed, 11 insertions, 2 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 9eeba614c7..148c1772bf 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -1020,10 +1020,11 @@ let lia (can_enum : bool) (prfdepth : int) sys = p) sys end; + let bnd1 = bound_monomials sys in let sys = subst sys in - let bnd = bound_monomials sys in + let bnd2 = bound_monomials sys in (* To deal with non-linear monomials *) - let sys = bnd @ saturate_by_linear_equalities sys @ sys in + let sys = bnd1 @ bnd2 @ saturate_by_linear_equalities sys @ sys in let sys' = List.map (fun ((p, o), prf) -> (cstr_of_poly (p, o), prf)) sys in xlia (List.map fst sys) can_enum reduction_equations sys' diff --git a/test-suite/micromega/bug_12790.v b/test-suite/micromega/bug_12790.v new file mode 100644 index 0000000000..39d640ebd9 --- /dev/null +++ b/test-suite/micromega/bug_12790.v @@ -0,0 +1,8 @@ +Require Import Lia. + +Goal forall (a b c d x: nat), +S c = a - b -> x <= x + (S c) * d. +Proof. +intros a b c d x H. +lia. +Qed. |