diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-06-18 14:59:56 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-06-18 14:59:56 +0200 |
| commit | 74aa0e2a6879e2bd062a881bc5fc474374d3c357 (patch) | |
| tree | 1d778cdc7794677f0f5a91ab9d1a83df5b86af49 | |
| parent | 698c8ffb48bf01356bda052711bed074662b2401 (diff) | |
| download | smtcoq-74aa0e2a6879e2bd062a881bc5fc474374d3c357.tar.gz smtcoq-74aa0e2a6879e2bd062a881bc5fc474374d3c357.zip | |
Corrected a bug in the generation of certificates for CNF computation of iff
| -rw-r--r-- | src/trace/smtCnf.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/trace/smtCnf.ml b/src/trace/smtCnf.ml index d159db0..f2a06c8 100644 --- a/src/trace/smtCnf.ml +++ b/src/trace/smtCnf.ml @@ -129,7 +129,7 @@ module MakeCnf (Form:FORM) = let na, nb = Form.neg a, Form.neg b in link_Other (BuildDef nl) [nl;a;nb]; link_Other (BuildDef pl) [pl;na;nb]; - link_Other (BuildDef2 nl) [pl;na;b]; + link_Other (BuildDef2 nl) [nl;na;b]; link_Other (BuildDef2 pl) [pl;a;b]; set_done l; cnf a; |