watcher stack overflow

[gipsyh]

Now on sub-ILA:AES_BLOCK

Start checking sub-instruction: LOAD
Parsing file "wrapper.v"... DONE
Parsing file "rst.ets"... DONE
Solving "variable_map_assert_0" *** internal error in 'lglib.c': watcher stack overflow
Finish: LOAD

[zhanghongce]

Hi Yuheng, I suspect that this has something to do with the CoSA installation. wonder how CoSA was installed. Are you using the docker image?

[gipsyh]

Hi Yuheng, I suspect that this has something to do with the CoSA installation. wonder how CoSA was installed. Are you using the docker image?

I'm not using docker.
I installed CoSA by pip3.
When I use z3 as solver, there is no problem.

Thanks!

[zhanghongce]

Thanks for the info. However, I'm afraid that this is out of our scope. As you see it is something deep in the lingeling SAT solver which is subsequently used in the SMT solver.

https://github.com/arminbiere/lingeling/blob/72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee/lglib.c#L3746

What I would like to suggest is to try configuring the SMT solver (say Boolector, if it is an error when you used Boolector) to use another SAT solver (say Cadical) and rebuild Boolector to work around this.

[gipsyh]

ok, thanks for your help!