diff options
| author |  boehmes <unknown> | 2012-09-27 17:13:42 +0200 |
|---|---|---|
| committer | boehmes <unknown> | 2012-09-27 17:13:42 +0200 |
| commit | 623a87c132abec61b5c74a6a00a7b162073a6a8d (patch) | |
| tree | b95ba791592cf395ce99035715de98578a5519ee /Test/prover | |
| parent | ed83becd12d7079e6ce2853fbebace20b1e7df5a (diff) | |
Boogie: new syntax for integer division and modulus: use div and mod instead of / and %
Diffstat (limited to 'Test/prover')
| -rw-r--r-- | Test/prover/EQ_v2.Eval__v4.Eval_out.bpl | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl index e4da94f4..e53e00b4 100644 --- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl +++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl @@ -382,7 +382,7 @@ axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y);
-axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x / y);
+axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y);
axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y);
@@ -1173,7 +1173,7 @@ axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y);
-axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x / y);
+axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y);
axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y);
|