diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-09 09:18:29 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-09 09:18:29 +0100 |
| commit | 517b6ba3bb029470bdb3f230188af1f398b14a91 (patch) | |
| tree | fb20cff576d97e148d03c40d4543b7ddc8fc0f22 /src/options/bv_bitblast_mode.h | |
| parent | 4ec1c04f28293386518582b0257345f84461350d (diff) | |
Clause proof printing (#2779)
* Print LFSC proofs of CNF formulas
* Unit Test for clause printing
* Added SAT input proof printing unit test
* Fixed cnf_holds reference. Proofs of CMap_holds
There were references to clauses_hold, which should have been references
to cnf_holds.
Also added a function for printing a value of type CMap_holds, and a
test for this function.
Diffstat (limited to 'src/options/bv_bitblast_mode.h')
0 files changed, 0 insertions, 0 deletions