Merge PR #12815: [micromega] Fix bug#12790

Reviewed-by: vbgl

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.