search

PrincetonUniversity / IMDb-Archive

ILA Model Database
MIT License
20 stars 4 forks source link

watcher stack overflow #29

Open gipsyh opened 2 years ago

gipsyh commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

ok, thanks for your help!