From 36548d6634864a131cc83ce21491c797163de305 Mon Sep 17 00:00:00 2001
From: QGarchery <QGarchery@users.noreply.github.com>
Date: Mon, 3 Dec 2018 08:08:56 +0100
Subject: verit also works when it doesn't use the conclusion (#24)

Fixes issue #20
---
 src/trace/smtForm.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/trace/smtForm.ml')

diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index c408343..d2e039b 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -449,7 +449,9 @@ module Make (Atom:ATOM) =
 
     (** Producing Coq terms *)
 
-    let to_coq hf = mkInt (to_lit hf)
+    let to_coq hf = let i = to_lit hf in
+                    if i < 0 then failwith "This formula should'nt be in Coq"
+                    else mkInt i
 
     let args_to_coq args =
       let cargs = Array.make (Array.length args + 1) (mkInt 0) in
-- 
cgit