Using keys() produces incorrect UCLID5 code with PVerifier backend #932
Description
❯ p --version
P version 3.0.2.0
~~ [PTool]: Thanks for using P! ~~
❯ uclid --help
uclid 0.9.5
uclid is from a4e4e7a22780833c86d6a650af2fcf88a7d00a06
p is from 7c313ac4115131a0351cee407fdb9cca7819c349
Here's the code to reproduce this error
machine Foo {
var m: map[int, int];
start state A {
entry {
var i: int;
foreach(i in keys(m)) {
}
}
}
}
Running p compile (with *.pproj setting backend to PVerifier)
Code generation for PVerifier...
Generated 2 files for OneBackup_default
Generated 1 files for OneBackup_full
Compiling generated code...
Proving: default
🔍 Checked 0/2 goals...[PVerifier Compiling Generated Code:]
Verifying generated UCLID5 code FAILED (f813fd28828b23fd49a134969bc97914.ucl)!
Syntax error on line 64: Syntax Error after keyword while.
while (PChecklist_integerPOption_integer != PLocal_m)
[THIS SHOULD NOT HAVE HAPPENED, please report it to the P team or create a GitHub issue]
Verifying generated UCLID5 code FAILED (f813fd28828b23fd49a134969bc97914.ucl)!
Syntax error on line 64: Syntax Error after keyword while.
while (PChecklist_integerPOption_integer != PLocal_m)
I found that seq was not able to be used with PVerifer but the following code does works which is interesting.
// Change keys() to keys_() then the UCLID5 error disappear.
pure keys_(m: map[int, int]): set[int];
init-condition forall (k: int, m: map[int, int]) :: k in m ==> k in keys_(m);
invariant a: forall (k: int, m: map[int, int]) :: k in m ==> k in keys_(m);