[SAL] sal-inf-bmc VS sal-bmc

[Bruno Dutertre]

Peter Bokor wrote:
> Dear All,
> 
>  
> 
> As far as I know sal-inf-bmc differs from sal-bmc in that the former makes
> calls to an SMT and the latter to a SAT solver. 
> 
>  
> 
> Recently, I experienced that a finite model could be verified faster with
> sal-inf-bmc than with sal-bmc. The bottle neck of the proof seemed to be the
> "unfolding of quantifiers" and "unfolding of initialization". My model has a
> tricky definition of an interpreted function f where I make restrictions to
> the general case:  f IN {v:[type1 -> type2]|condition}.
> 
>  
> 
> It seems that the SMT solver can handle this better than the SAT solver.
> Btw, why does SAL have sal-inf-bmc and sal-bmc, why not only sal-inf-bmc? 
> 
> 

Peter,

There's no general rule on this. For some systems, bmc works better, for
others inf-bmc is better. Obviously, representing a function using
bits has a very high overhead so finite bmc is at a disadvantage in
such cases, but that's not true overall.

Bruno

> 
> Hmm, maybe my question concerns more Yices than SAL, but I experienced this
> problem with SAL so here I send it :)
> 
>  
> 
> Thanks
> 
>  
> 
> Peter
> 
>  
> 
>  
> 
> 


-- 
Bruno Dutertre                             | bruno at csl.sri.com
CSL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717