Project

General

Profile

Actions
Copy link

Bug #544

closed

CVC3 is too slow and greedy in memory consumption

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

Status:
Closed
Priority:
Normal
Assignee:
Pavel Shved
Category:
-
Target version:
2.6
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 open — 2 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
Copy link
 #1

Updated by Pavel Shved almost 14 years ago

  • Status changed from Open to Resolved
Actions
Copy link
 #2

Updated by Alexey Khoroshilov over 13 years ago

Should we close it?

Actions
Copy link
 #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
Copy link
 #4

Updated by Pavel Shved over 13 years ago

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

Updated by Pavel Shved over 13 years ago

  • Target version set to 2.6
Actions
Copy link

Also available in: Atom PDF