[SAL-HELP] SAL 2.4 SMC --enable-slicer --enable-dynamic-reorder

[Bruno Dutertre]

Aron Sisak wrote:
> Hello,
> 
> I try to use the SAL (2.4 pre-release) SMC solver with both options
> --enable-slicer and --enable-dynamic-reorder. However, ICS is not
> distributed with this version. This makes SAL complain:
> 
> Error: Error executing ICS. The following command was used to execute ICS:
> ics -pp sexpr "/tmp/sal-aron-5212-input.ics" >
> "/tmp/sal-aron-5212-output.ics" 2> /dev/null
> If this is not the correct command to execute ICS, it can be changed
> using the statement:
> 
>   (sal/set-ics-command! "<path-to-ics>/ics")
> 
> However, if I install ICS, it dies with the following error message:
> ics: mlgmp41.c:1072: _mlgmp_q_create: Assertion `alloc_init_mpq() >
> 0x10000' failed.
> 
> (both the version supplied with SAL 2.3 and the one from the ICS 2.0
> distribution)
> I use Ubuntu GNU/Linux 6.10  (The Edgy Eft) on x86 (libgmp 3.4.1)
> 
> I also tried to use Yices 1.0 -- that runs perfectly with sal-bmc 2.4 --
> however I cannot "guess" the proper syntax. It gives the same error
> message as above.
> 
> Can you help me either to run ICS or to use Yices?
> Which is the preferred solution, if there is any?
> 
> Thanks in advance,
> 

Aron,

The slicer in the pre-release version of sal-2.4 currently
requires ICS. We're planning to release a better sal-2.4
(open source) in a few days, that uses yices by default.
This should fix these issues.

Best regards,

Bruno