Project

General

Profile

Actions

Bug #511

closed

SMTlib interface spends too much time generating predicates

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

Status:
Closed
Priority:
Urgent
Assignee:
Category:
-
Target version:
Start date:
10/29/2010
Due date:
12/02/2010
% Done:

0%

Estimated time:
Detected in build:
all of them
Platform:
Published in build:
f252fe5

Description

The mechanism to decrease the number of interpolation calls relies on getting only significant blocks from an error trace. It is done by adding block predicates one-by-one into a big conjunction, and testing it for satisfiability.

SMTlib interface in BLAST is implemented in such a way that at each satisfiability test the whole conjunction is converted to the SMTlib format. This way each minterm undergoes the same conversion over and over.

According to profiling results, this is a bottleneck in error trace analysis. So this should be fixed.


Files

Actions

Also available in: Atom PDF