[SAL-HELP] SAL 2.4 SMC --enable-slicer --enable-dynamic-reorder
Aron Sisak
aron at inf.bme.hu
Mon Dec 4 15:56:12 PST 2006
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,
--
Áron
More information about the SAL-HELP
mailing list