diff options
| author | QGarchery <QGarchery@users.noreply.github.com> | 2018-12-03 08:08:56 +0100 |
|---|---|---|
| committer | ckeller <ckeller@users.noreply.github.com> | 2018-12-03 08:08:56 +0100 |
| commit | 36548d6634864a131cc83ce21491c797163de305 (patch) | |
| tree | 283b642e4cdb593ee6add5c4bdeb0ccec1a9258d /src/trace/smtForm.ml | |
| parent | 3fdc107b26f475c8fe8b7052de826405b88c14b3 (diff) | |
| download | smtcoq-36548d6634864a131cc83ce21491c797163de305.tar.gz smtcoq-36548d6634864a131cc83ce21491c797163de305.zip | |
verit also works when it doesn't use the conclusion (#24)
Fixes issue #20
Diffstat (limited to 'src/trace/smtForm.ml')
| -rw-r--r-- | src/trace/smtForm.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |