Project

General

Profile

Actions

Bug #544

closed

CVC3 is too slow and greedy in memory consumption

Added by Pavel Shved over 13 years ago. Updated over 12 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

Also available in: Atom PDF