Double free for simple example

[parttimenerd]

I just ran the simple example from the homepage (and removed all to have a main method with just a single assert) and got the following:

build/sharpPI -i @I -o O main.cnf
sharpPI -- 1.1 from 2021-07-16T11:17:20Z
free(): double free detected in tcache 2
[1]    585710 abort (core dumped)  build/sharpPI -i @I -o O main.cnf

Any ideas?

[wadoon]

Could you provide the main.cnf?

[parttimenerd]

p cnf 1 1
1 0
c abc

results in

sharpPI -- 1.1 from 2021-07-16T11:17:20Z
free(): double free detected in tcache 2
Aborted (core dumped)

and

p cnf 1 1
1 0

results in

sharpPI -- 1.1 from 2021-07-16T11:17:20Z
[       0] Operation Mode: Bucket-wise (deterministic)
terminate called after throwing an instance of 'std::out_of_range'
  what():  vector::_M_range_check: __n (which is 0) >= this->size() (which is 0)
Aborted (core dumped)

[parttimenerd]

The original cnf file:
main.log

[wadoon]

Please have a look into the main.cnf. You should notice that the variables I and O do not have entries in the commented variables. Probably, they are removed during formulae slicing by CBMC. But #PI requires these information to determine on which variables it should project on.

This leads to an empty array of projected variables, which results into a strange exception.