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
 #1

Updated by Pavel Shved about 13 years ago

  • Status changed from Open to Resolved

After some debugging, it appears that the large numbers in the input data just made the Interpolating Prover yield wrong Lagrange coefficients.

For instance, this query

& [ = S96 4294967295 = S142 1 ] ; & [ & [ true = S180 + [ S142 1 ] <= S180 1 ] ]

yields the following interpolant:
<= * -2 S96 -8589934590

the L-s being
(incorrect) lambdas are: 4.65661287416e-10, 0., 0., 0.
(  correct) lambdas are: 0., 2., 2., -2.

To fix this, I added an option to tune CSIsat's arguments, and made it use "exact" linear constraints solving algorithm (with rational arithmetics). With it, it yields the correct interpolant for the given sample; still, it is not verified correctly, as the SAT exception is caught later on.

I'll check if we don't timeout too often, as the "exact" algorithm is slower than the default one.

Actions
Copy link
 #2

Updated by Pavel Shved about 13 years ago

  • Status changed from Resolved to Closed

No more strange issues of this sort

Actions
Copy link

Also available in: Atom PDF