From faaa2848c37444f8f37ac432c25f9f813e1df39b Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Sat, 27 Oct 2018 20:08:44 +0200
Subject: Adding support for lemmas in the command verit

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

(limited to 'src/lia/lia.ml')

diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index 589d59a..e5f2fe9 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -160,6 +160,7 @@ let rec smt_Form_to_coq_micromega_formula tbl l =
           failwith "Lia.smt_Form_to_coq_micromega_formula: wrong number of arguments for Fnot2"
         else
           smt_Form_to_coq_micromega_formula tbl l.(0)
+      | Fapp (Fforall _, _) -> assert false
   in
   if Form.is_pos l then v
   else N(v)
-- 
cgit