search

c4-project / c4f

The C4 Concurrent C Fuzzer
MIT License
14 stars 1 forks source link

State comparator seems to be confusing witnesses and counter-examples #144

Closed MattWindsor91 closed 5 years ago

MattWindsor91 commented 5 years ago

I might have accidentally flipped a flag somewhere when refactoring.

MattWindsor91 commented 5 years ago

Aha. When there's a forall postcondition, the * flips from signifying a witness to signifying a counter-example.

MattWindsor91 commented 5 years ago

The clue is in the first bit of the Herd/Litmus observation record: it's Allowed in existential postconditions and Required in universal ones.