Re: [PATCH] cex: fix a crash

[Akim Demaille]

> Le 16 mai 2020 à 20:51, Vincent Imbimbo <address@hidden> a écrit :
> 
> * src/parse-simulation.c: Replace reference counting with parse_state_retain 
> everywhere.
> (free_parse_state): Make this function iterative instead of recursive. Long 
> parse_state chains were causing stack exhaustion.
> 
> * tests/counterexample.at: fix expectations
> 
> It's possible for the search to do a rapid infinite descent through 
> productions, which is one of the reasons there's a timeout. I had never 
> thought of the chance a path would be deep enough to cause stack exhaustion.
> 
> I'll be taking a deeper look into the actual results of these tests soon. I'm 
> curious as to what causes the unifying search to fail on the first example 
> from this test.

Hi Vincent,

This does not seem right.  You should try to use clang with address sanitizer 
(see .travis.yml for one way to set it up).  For instance, that's one failure 
on my machine, caused by this commit.

Cheers!

testsuite.log
Description: Binary data