Fix efficiency regression #11436

- The cutting plane has been (sometimes) improved to generate stronger
  cuts.
- There is now some support for profiling the Simplex
  see documentation for Show Lia Profile.

2 files changed, 22 insertions, 7 deletions

diff --git a/test-suite/micromega/bug_11436.v b/test-suite/micromega/bug_11436.v
new file mode 100644
index 0000000000..fc6ccbb233
--- /dev/null
+++ b/test-suite/micromega/bug_11436.v
@@ -0,0 +1,19 @@
+Require Import ZArith Lia.
+Local Open Scope Z_scope.
+
+Unset Lia Cache.
+
+Goal forall a q q0 q1 r r0 r1: Z,
+    0 <= a < 2 ^ 64 ->
+    r1 = 4 * q + r ->
+    0 <= r < 4 ->
+    a = 4 * q0 + r0 ->
+    0 <= r0 < 4 ->
+    a + 4 = 2 ^ 64 * q1 + r1 ->
+    0 <= r1 < 2 ^ 64 ->
+    r = r0.
+Proof.
+  intros.
+  (* subst. *)
+  Time lia.
+Qed.
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 9efb81a901..36b4243ef8 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -11,15 +11,14 @@ Open Scope Z_scope.
 
 Lemma Zabs_square : forall x,  (Z.abs  x)^2 = x^2.
 Proof.
- intros ; case (Zabs_dec x) ; intros ; nia.
+ intros ; nia.
 Qed.
-Hint Resolve Z.abs_nonneg Zabs_square.
 
 Lemma integer_statement :  ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0.
 Proof.
   intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p).
 assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2
-         /\ Z.abs p^2 = p^2) by auto.
+         /\ Z.abs p^2 = p^2) by auto using Z.abs_nonneg, Zabs_square.
 assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by
   (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; nia).
 generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
@@ -45,10 +44,7 @@ Proof.
   intros.
   destruct x.
   simpl.
-  unfold Z.pow_pos.
-  simpl.
-  rewrite Pos.mul_1_r.
-  reflexivity.
+  lia.
 Qed.
 
 Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.