From cef01e0069b8e6a26a74f3c6bb825a9a3c46ef60 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Fri, 15 May 2020 14:07:48 +0200
Subject: More precise call to Micromega

---
 src/lia/lia.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index 53ee55d..4444816 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -197,7 +197,7 @@ let smt_clause_to_coq_micromega_formula tbl cl =
 (* val tauto_lia : Mc.z formula -> Certificate.Mc.zArithProof list option *)
 let tauto_lia ff =
   let prover = linear_Z in
-  let cnf_ff,_ = cnf Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce  ff in
+  let cnf_ff,_ = Structures.Micromega_plugin_Coq_micromega.cnf Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce  ff in
   match witness_list_tags [prover] cnf_ff with
     | None -> None
     | Some l -> Some (List.map fst l)
-- 
cgit