Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
moved Minisat namespace into CVC4
|
|
|
|
|
|
|
|
This avoids conflicts when CVC4 is linked to an application that
also uses plain Minisat.
|
|
|
|
|
|
signature. Add regressions.
|
|
|
|
|
|
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
|
|
|
|
Thanks Johannes Kanig for the report.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fix compiler warnings in BV-related code (unused vars mostly).
|
|
|
|
|
|
|
|
|
|
This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(resolves bug #548).
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
|
|
Martin Brain for the patch!
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|