Boolector error: more than 134217724 variables message

[alessandro...@gmail.com]

Hi,

I am applying automated verification in energy area, with some interesting results . I am doing some improvement at my  tool, testing different solvers and model checkers.

Using Boolector version 2.4.1, I got the following message: 

Solving with solver Boolector 2.4.1

*** internal error in 'lglib.c': more than 134217724 variables

How can I solve this issue? Some advice?

(environment: Intel octa core Xeon CPU E5-2640 with 2.4 GHz and 264 GB of RAM, running Ubuntu 18.04.1 LTS 64-bits. Concerning

our verification engine, ESBMC v6.0.0 was used)

Thank you

Att. Alessandro Trindade

PhD Student of Informatics

Federal University of Amazonas - Brazil

[Armin Biere]

Lingeling has a 2^27 variable limit (to keep the memory footprint a factor 2 smaller

than for instance MiniSAT).  With CaDiCaL you can have really INT_MAX variables

(yes I have test cases and even DIMACS files which test this).   I am not sure whether

the rest of Boolector can really do this yet, but should be the case, since we do not use

any major bit-stuffing on integers, except maybe one or two bits.  Thus I assume this

should go through when you use CaDiCaL instead of Lingeling.   You might need to switch

off skeleton preprocessing which currently only works with Lingeling, to avoid running into

this limitation during preprocesing.  So

$ boolector -sp 0 --sat-engine=cadical

should do the trick ...

[Armin Biere]

Forgot to mention that CaDiCaL is only functional for QF_BV at this point.

Armin

On Thursday, January 10, 2019 at 4:14:45 PM UTC+1, Armin Biere wrote:

Lingeling has a 2^27 variable limit (to keep the memory footprint a factor 2 smaller

than for instance MiniSAT).  With CaDiCaL you can have really INT_MAX variables

(yes I have test cases and even DIMACS files which test this).   I am not sure whether

the rest of Boolector can really do this yet, but should be the case, since we do not use

any major bit-stuffing on integers, except maybe one or two bits.  Thus I assume this

should go through when you use CaDiCaL instead of Lingeling.   You might need to switch

off skeleton preprocessing which currently only works with Lingeling, to avoid running into

this limitation during preprocesing.  So

$ boolector -sp 0 --sat-engine=cadical

should do the trick ...

[BACHIRI Wahiba]

Hello , 

How can you change the SAT engine of boolector "as you mentioned:   boolector -sp 0 --sat-engine=cadical " in esbmc ?

[Armin Biere]

I think this is a question for the ESBMC developers as current Boolector from GitHub uses CaDiCaL anyhow as default SAT solver (assuming you have set it up during the build process).

Armin

--
You received this message because you are subscribed to the Google Groups "Boolector" group.
To unsubscribe from this group and stop receiving emails from it, send an email to boolector+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/boolector/b15e0b7a-ec33-4986-996f-d971dcf55389n%40googlegroups.com.

[Lucas Cordeiro]

Hello,

You can check ESBMC building instructions at https://github.com/esbmc/esbmc/blob/master/BUILDING.md.

In particular, we're using this command to build and set up Boolector in ESBMC:

git clone --depth=1 --branch=3.2.2 https://github.com/boolector/boolector && cd boolector && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh --prefix $PWD/../boolector-release && cd build && make -j9 && make install && cd .. && cd ..

So, currently, we're compiling ESBMC with Boolector 3.2.2 and the SAT solver Lingeling. Some time ago, we tried to use ESBMC with Boolector/CaDiCaL, but Boolector/Lingeling was still producing the highest scores in our evaluations.

Best,
Lucas

To view this discussion on the web visit https://groups.google.com/d/msgid/boolector/CANp8Ba1%3Dg0L5prkdYwbg71Rn5Sapjt%3DfJzX3wxLCGWYTJQzxhg%40mail.gmail.com.

--

Lucas C. Cordeiro​

https://ssvlab.github.io/lucasccordeiro/