[SAL-HELP] BDD reordering is too slow

[Bruno Dutertre]

Pinter Norbert wrote:
> Dear SAL users!
> 
> I'm a student at the Budapest University of Technology and Economics. I
> use the SAL model checker, and I have got a problem. When I use the
> sal-smc to prove my model, the process of the bdd reordering is too slow,
> but the time of the verification is not. I tried to save the reorder with
> the --reorder-output=filename, but if I start the sal-smc with the
> --reorder-input=filename again, then the model checker restart the bdd
> reordering phase. Can I somehow save the reordered bdd and load it back
> after the first run? Exist any solution about my problem?
> Thanks the help!
> 
> Best regards,
> Norbert Pintér
> 

Hi Norbert,

The --input-order option specifies an initial variable order to use.
It does not prevent BDD reordering during construction of the
transition relation. You have to explicitly disable BDD reordering
by giving the command-line option -r none (or --reorder-method=none).

There are other flags you could give to sal-smc that should in principle
have the same effect. However there's a bug in SAL and some of these
flags are not interpreted properly. That will be fixed in future
releases.

Bruno