BMC fails while induction proof succeeds

[kentindell]

BMC is failing but what I think it happening is that the assert/assume swap is being carried to later read files. The problem comes from something like this:

read -formal -assert-assumes -assume-asserts ../../../a_f.v
read -formal -assert-assumes -assume-asserts ../../../b_f.v
read -formal ../../../c_f.v
read -formal ../../../c.v

In the above, there are three modules (A, B, C), each with a 'contract' (_f suffix). The .sby file is set up to verify module C against its own contract and the contracts of the other two modules. This is why the assert/assumes are swapped over for the A and B contracts (since C is a client module). In my code this fails bmc (regardless of engine) and passes prove. The BMC fails with an error in c.v on a line with an assume statement, but the error message calls it an assertion failure.

If I change the order of the file reading to:

read -formal ../../../c_f.v
read -formal ../../../c.v
read -formal -assert-assumes -assume-asserts ../../../a_f.v
read -formal -assert-assumes -assume-asserts ../../../b_f.v;

Then bmc doesn't fail (and prove succeeds). It seems as if the assert/assume swapping is somehow being carried over from one line read to the next.

Is this a bug? Am I misunderstanding something? Have I missed something completely obvious?

[KrystalDelusion]

This does indeed appear to be a bug in Yosys where the flag for assert-assumes is set high, but never set low (assume-asserts however appears to be set correctly).