Project

General

Profile

Actions
Copy link

Bug #1850

closed

Interpolants of some useful blocks sometimes have nothing to do with the blocks!

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

Status:
Closed
Priority:
Urgent
Assignee:
Pavel Shved
Category:
-
Target version:
2.7
Start date:
09/30/2011
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

For the cill-ed file drivers-net-wan-farsync from the competition set (attached), options:

pblast.opt -alias bdd -cref -cldepth 3 -nomusts -lattice -include-lattice symb -stop-sep -merge bdd -skipnorm -ialias -iclos -nolabelmeanssafe -ignoredupfn -enable-recursion -nosserr

Blocks:
[INF0] 1 : 86:   Block( ... fst_pci_dev_id[ 0 ].subdevice = 4294967295 ...)
[INF0] 53 : 4718:        Block(ldv_module_refcounter = ldv_module_refcounter  +  1;)
[INF0] 69 : 4736:        Pred(ldv_module_refcounter  <=  1)
...
addPred: 0: (gui) adding predicate (fst_pci_dev_id[ (0)  ]).subdevice*-2<=-8589934590 to the system

This leads to NoNewPredicates Exception, and we lose points. :-(

Files

BLAST_AUTO.i (923 KB) BLAST_AUTO.i driver that fails Pavel Shved, 09/30/2011 06:35 PM
Actions
Copy link

Also available in: Atom PDF