1
Vote

Issue with NonDet in Real Machines

description

Type checking in P has some bug. NonDet are allowed in real machines.
I have attached 2 examples which should fail.

Also, I don't completely understand the reason/need of allowing non-det to ghost variables in real machines.

file attachments

comments

ankushd wrote Oct 8, 2013 at 6:31 PM

The example in
\Tests\Pos\Nondet\NonDetExp.p should not be allowed