Project

General

Profile

Actions
Copy link

Bug #545

closed

CVC3 wastes some time after it has already given an answer

Added by Pavel Shved over 13 years ago. Updated over 12 years ago.

Status:
Rejected
Priority:
Low
Assignee:
Pavel Shved
Category:
-
Target version:
2.6
Start date:
11/14/2010
Due date:
% Done:

0%

Estimated time:
Detected in build:
cvc3: 0e2a0c93
Platform:
Published in build:

Description

I noticed that after CVC3 already printed its answer (whether the input formula is SAT), it spends some time doing something.

For example, I run the file attached (smt_query_long) with the following command:

cvc3 -lang smtlib  < smt_query_long

The program runs for 18 seconds (and takes 2 Gb of memory on my 64-bit machine). However, it prints its answer on 12th second, wasting 30% of its time for doing...nothing. For all this period, the two-gigabyte memory blob hangs in RAM, shrinking only for a tiny bit.

I bet the issues is how CVC3's memory allocator works. Could this be optimized somehow?

I use CVC3 revision 0e2a0c93 (for-blast branch).

Files

smt_query_long (89.5 KB) smt_query_long SMTlib query that runs for a long time Pavel Shved, 11/14/2010 01:49 PM

Related issues 1 (0 open — 1 closed)

Blocks BLAST - Bug #544: CVC3 is too slow and greedy in memory consumptionClosedPavel Shved11/14/2010

Actions
Actions
Copy link

Also available in: Atom PDF