summaryrefslogtreecommitdiff
path: root/proofs/signatures/th_arrays.plf
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-03-13 22:47:04 +0000
committerGitHub <noreply@github.com>2019-03-13 22:47:04 +0000
commitb574ccf82270f8887d2d697c537c591ff4ab68a2 (patch)
treeeaecd85977bda2808e06618b981d16b60e2f5639 /proofs/signatures/th_arrays.plf
parent68174dedcb4bf9d91241585ab1cc876d2fa83d62 (diff)
Add statistics for proof gen./checking time, size (#2850)
This commit adds a statistic that records the total size of all proofs generated by an instance of `SmtEngine`. The commit also moves `SmtEngine::checkProof()` into `smt_engine.cpp` because it needs to know the complete type of `d_stats` (and the separate file for that method didn't seem that useful). Additionally, it changes `smt::SmtEngine::checkProofTime` to `smt::SmtEngine::lfscCheckProofTime` that only measures the time spent in LFSC and adds a statistic `proof::ProofManager::proofProductionTime` that measures the proof production time separately (also works with `get-proof`/`--dump-proof`).
Diffstat (limited to 'proofs/signatures/th_arrays.plf')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback