From 6f1634d2f822037a482436a64d3ef3bfb2fac2a0 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Fri, 8 Mar 2019 09:56:49 +0100
Subject: Several improvements and fixes of Lia

- Improved reification for Micromega (support for #8764)

- Fixes #9268: Do not take universes into account in lia reification

  Improve #9291 by threading the evar_map during reification.
  Universes are unified.

- Remove (potentially cyclic) dependency over lra for Rle_abs

- Towards a complete simplex-based lia

  fixes  #9615

Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal  for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.

For scalability, nia is currently NOT performing this pre-processing.

- Lia is using the FSet library

  manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
  to work around a "leaked" hint breaking compatibility of eauto
---
 test-suite/output/MExtraction.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index 36992e4dda..7429a521b3 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -7,6 +7,8 @@ Require Import QMicromega.
 Require Import RMicromega.
 
 Recursive Extraction
-   List.map simpl_cone (*map_cone  indexes*)
-   denorm Qpower vm_add
+           Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
+           ZMicromega.cnfZ ZMicromega.bound_problem_fr QMicromega.cnfQ
+           List.map simpl_cone (*map_cone  indexes*)
+           denorm Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
-- 
cgit v1.2.3