Actions
Bug #544
closedCVC3 is too slow and greedy in memory consumption
Start date:
11/14/2010
Due date:
% Done:
0%
Estimated time:
Detected in build:
none
Platform:
Published in build:
Description
The default shipment of ldv-tools contains CVC3 solver, which is capable to processing SMTlib language. This solver is a good one, but it consumes too much of resources: both time and memory.
Perhaps, we can tweak its performance, so that it becomes faster and less greedy? Maybe, there are tweaks and patches that can trade it for precision of analysis?..
This issue is a tracker for all such bugs and problems found in CVC3 solver.
Updated by Pavel Shved over 13 years ago
- Status changed from Resolved to Closed
Ok, closing as CVC3 is not a bottleneck with the current default settings. Without lattices, however, it takes up to 2/3 of the total CPU time, but that's not default today. Will reopen when CVC3 would be the major bottleneck again.
Updated by Pavel Shved about 13 years ago
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)
Actions