Project

General

Profile

Actions

Bug #544

closed

CVC3 is too slow and greedy in memory consumption

Added by Pavel Shved almost 14 years ago. Updated about 13 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Category:
-
Target version:
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.


Related issues 2 (0 open2 closed)

Blocked by BLAST - Bug #545: CVC3 wastes some time after it has already given an answerRejectedPavel Shved11/14/2010

Actions
Blocked by BLAST - Feature #546: Could CVC3 runtime be improved by decreasing precision?ClosedMikhail Mandrykin11/14/2010

Actions
Actions #1

Updated by Pavel Shved over 13 years ago

  • Status changed from Open to Resolved
Actions #2

Updated by Alexey Khoroshilov over 13 years ago

Should we close it?

Actions #3

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.

Actions #4

Updated by Pavel Shved about 13 years ago

  • Project changed from Linux Driver Verification to BLAST
  • Category deleted (BLAST)
Actions #5

Updated by Pavel Shved about 13 years ago

  • Target version set to 2.6
Actions

Also available in: Atom PDF