Boogie: new syntax for integer division and modulus: use div and mod instead of / and %

4 files changed, 4 insertions, 4 deletions

diff --git a/Test/livevars/bla1.bpl b/Test/livevars/bla1.bpl
index 2854e5df..12ccc44a 100644
--- a/Test/livevars/bla1.bpl
+++ b/Test/livevars/bla1.bpl
@@ -471,7 +471,7 @@ function {:inline true} INT_NEQ(x:int, y:int)  returns  (bool)   {x != y}
 function {:inline true} INT_ADD(x:int, y:int)  returns  (int)   {x + y}

 function {:inline true} INT_SUB(x:int, y:int)  returns  (int)   {x - y}

 function {:inline true} INT_MULT(x:int, y:int) returns  (int)   {x * y}

-function {:inline true} INT_DIV(x:int, y:int)  returns  (int)   {x / y}

+function {:inline true} INT_DIV(x:int, y:int)  returns  (int)   {x div y}

 function {:inline true} INT_LT(x:int, y:int)   returns  (bool)  {x < y}

 function {:inline true} INT_ULT(x:int, y:int)   returns  (bool)  {x < y}

 function {:inline true} INT_LEQ(x:int, y:int)  returns  (bool)  {x <= y}

diff --git a/Test/livevars/daytona_bug2_ioctl_example_1.bpl b/Test/livevars/daytona_bug2_ioctl_example_1.bpl
index 1decba12..ae8ff08c 100644
--- a/Test/livevars/daytona_bug2_ioctl_example_1.bpl
+++ b/Test/livevars/daytona_bug2_ioctl_example_1.bpl
@@ -510,7 +510,7 @@ function {:inline true} INT_NEQ(x:int, y:int)  returns  (bool)   {x != y}
 function {:inline true} INT_ADD(x:int, y:int)  returns  (int)   {x + y}

 function {:inline true} INT_SUB(x:int, y:int)  returns  (int)   {x - y}

 function {:inline true} INT_MULT(x:int, y:int) returns  (int)   {x * y}

-function {:inline true} INT_DIV(x:int, y:int)  returns  (int)   {x / y}

+function {:inline true} INT_DIV(x:int, y:int)  returns  (int)   {x div y}

 function {:inline true} INT_LT(x:int, y:int)   returns  (bool)  {x < y}

 function {:inline true} INT_ULT(x:int, y:int)   returns  (bool)  {x < y}

 function {:inline true} INT_LEQ(x:int, y:int)  returns  (bool)  {x <= y}

diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl b/Test/livevars/daytona_bug2_ioctl_example_2.bpl
index 0b49364b..44e51827 100644
--- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl
+++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl
@@ -521,7 +521,7 @@ function {:inline true} INT_NEQ(x:int, y:int)  returns  (bool)   {x != y}
 function {:inline true} INT_ADD(x:int, y:int)  returns  (int)   {x + y}

 function {:inline true} INT_SUB(x:int, y:int)  returns  (int)   {x - y}

 function {:inline true} INT_MULT(x:int, y:int) returns  (int)   {x * y}

-function {:inline true} INT_DIV(x:int, y:int)  returns  (int)   {x / y}

+function {:inline true} INT_DIV(x:int, y:int)  returns  (int)   {x div y}

 function {:inline true} INT_LT(x:int, y:int)   returns  (bool)  {x < y}

 function {:inline true} INT_ULT(x:int, y:int)   returns  (bool)  {x < y}

 function {:inline true} INT_LEQ(x:int, y:int)  returns  (bool)  {x <= y}

diff --git a/Test/livevars/stack_overflow.bpl b/Test/livevars/stack_overflow.bpl
index 242acd65..fae3e863 100644
--- a/Test/livevars/stack_overflow.bpl
+++ b/Test/livevars/stack_overflow.bpl
@@ -831,7 +831,7 @@ function {:inline true} INT_NEQ(x:int, y:int)  returns  (bool)   {x != y}
 function {:inline true} INT_ADD(x:int, y:int)  returns  (int)   {x + y}

 function {:inline true} INT_SUB(x:int, y:int)  returns  (int)   {x - y}

 function {:inline true} INT_MULT(x:int, y:int) returns  (int)   {x * y}

-function {:inline true} INT_DIV(x:int, y:int)  returns  (int)   {x / y}

+function {:inline true} INT_DIV(x:int, y:int)  returns  (int)   {x div y}

 function {:inline true} INT_LT(x:int, y:int)   returns  (bool)  {x < y}

 function {:inline true} INT_ULT(x:int, y:int)   returns  (bool)  {x < y}

 function {:inline true} INT_LEQ(x:int, y:int)  returns  (bool)  {x <= y}