diff options
| author |  stefanheule <unknown> | 2012-09-30 11:47:51 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-09-30 11:47:51 +0200 |
| commit | 1e42c8cd6fd921c69f1bf7340c05feebd0c11a88 (patch) | |
| tree | ff124431435e08245117f355abc1f9dc8ff1f23b /Chalice | |
| parent | 65e23620d56b5844a34b7919cad5a2b586029e28 (diff) | |
Chalice: Use new 'mod' and 'div' operators of Boogie for division and modulo.
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/main/scala/Boogie.scala | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Chalice/src/main/scala/Boogie.scala b/Chalice/src/main/scala/Boogie.scala index f7666ec1..e775b688 100644 --- a/Chalice/src/main/scala/Boogie.scala +++ b/Chalice/src/main/scala/Boogie.scala @@ -66,8 +66,8 @@ object Boogie { def +(that: Expr) = BinaryExpr("+", this, that)
def -(that: Expr) = BinaryExpr("-", this, that)
def *(that: Expr) = BinaryExpr("*", this, that)
- def /(that: Expr) = BinaryExpr("/", this, that)
- def %(that: Expr) = BinaryExpr("%", this, that)
+ def /(that: Expr) = BinaryExpr("div", this, that)
+ def %(that: Expr) = BinaryExpr("mod", this, that)
def := (that: Expr) = Assign(this, that)
def apply(e: Expr, f: Expr) = new MapSelect(this, e, Some(f))
def apply(e: Expr) = new MapSelect(this, e, None)
|