From 74932ad2ff431f49370d8bb0f730a588b192b484 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 10 Aug 2020 16:45:35 +0200
Subject: [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
---
 plugins/micromega/certificate.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins')

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'
 
-- 
cgit v1.2.3