Bug in `modelcheck`
The following command :
modelcheck --bloemen-ec --formula '"P.a==2" | "P.b==3"' --model ./ltsmin/finite.dve -p 1 --csv
segfaults. Apparently the problem comes from line 197 of mc_instanciator.hh
. Removing this delete
leaks but works perfectly. GDB locates this segfault inside the fixpool
destructor.
Maybe merging something gets wrong while merging twacube
, since there were a last update just before merging?
Nonetheless, this is very strange since the following command run perfectly (ie. only changing the algorithm)
modelcheck --bloemen --formula '"P.a==2" | "P.b==3"' --model ./ltsmin/finite.dve -p 1 --csv
You should note that most of the structure of bloemen.hh
and bloemen_ec.hh
are similar.
No idea for now where comes from the problem