diff options
| author |  Unknown <pmueller@peter2.d.ethz.ch> | 2011-07-16 01:16:04 +0200 |
|---|---|---|
| committer | Unknown <pmueller@peter2.d.ethz.ch> | 2011-07-16 01:16:04 +0200 |
| commit | 2ac0f210996c33bef7075a5e27e805a2730311a6 (patch) | |
| tree | f35d3ad4b9fad453c52cee9b1a9c70acd8e55cce /Chalice | |
| parent | 2f7dd71225c89e0901bf228203d88b73814d9354 (diff) | |
Suppress generation of Drop(s, 0). This expression caused unnecessary verification problems, even though the axioms should be sufficient to handle this case (and also trigger).
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/Translator.scala | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index ea05d4bc..552fa906 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -1668,7 +1668,12 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E createAppendSeq(Tr(e0), Tr(e1))
case at@At(e0, e1) =>SeqIndex(Tr(e0), Tr(e1))
case Drop(e0, e1) =>
- Boogie.FunctionApp("Seq#Drop", List(Tr(e0), Tr(e1)))
+ e1 match {
+ case IntLiteral(0) =>
+ Tr(e0)
+ case _ =>
+ Boogie.FunctionApp("Seq#Drop", List(Tr(e0), Tr(e1)))
+ }
case Take(e0, e1) =>
Boogie.FunctionApp("Seq#Take", List(Tr(e0), Tr(e1)))
case Length(e) => SeqLength(Tr(e))
|