Skip to content

Commit

Permalink
Update test-instance-procedure-calls-1.ucl
Browse files Browse the repository at this point in the history
  • Loading branch information
polgreen committed May 9, 2024
1 parent b0c07a9 commit ef99e4e
Showing 1 changed file with 4 additions and 13 deletions.
17 changes: 4 additions & 13 deletions test/test-instance-procedure-calls-1.ucl
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
/*
KNOWNBUG: Instance procedure calls from next block use new value.
PREVIOUS BUG: Instance procedure calls from next block use new value.
- When calling proc1(), proc2() from sub module, things are as expected.
- When calling proc1(), followed by proc2() from main module,
proc2 picks up the modified value of x, leading to an assertion failure.

Some issue with the inlining procedure from ModuleInstantiatorPass.

If the bug is fixed, this test should pass
*/


Expand Down Expand Up @@ -35,20 +36,10 @@ module sub

next
{
// call () = proc2();
// call () = proc2();
// call () = proc1();
// step' = step + 1;
}

// invariant a : (step == 1) ==> (y == 1);

// control
// {
// vobj = bmc(4);
// check;
// print_results;
// vobj.print_cex(x, y, step);
// }
}

module main {
Expand Down

0 comments on commit ef99e4e

Please sign in to comment.