From e9c589851d913a6566c421c87483dc7e94519f91 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Mon, 8 Feb 2016 12:28:25 -0800
Subject: Fix issue 124. Consider math operators that later turned into
 function calls as candidates for triggers.

---
 Source/Dafny/Triggers/TriggersCollector.cs | 26 ++++++++++++++++++++++++++
 Test/dafny4/Bug124.dfy                     | 14 ++++++++++++++
 Test/dafny4/Bug124.dfy.expect              |  2 ++
 3 files changed, 42 insertions(+)
 create mode 100644 Test/dafny4/Bug124.dfy
 create mode 100644 Test/dafny4/Bug124.dfy.expect

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index f96d3e4c..4204cc29 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -198,6 +198,7 @@ namespace Microsoft.Dafny.Triggers {
           expr is OldExpr || 
           expr is ApplyExpr || 
           expr is DisplayExpression ||
+          TranslateToFunctionCall(expr) ||
           (expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944
           (expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) {
         annotation = AnnotatePotentialCandidate(expr);
@@ -227,6 +228,31 @@ namespace Microsoft.Dafny.Triggers {
       return annotation;
     }
 
+    // math operations can be turned into a Boogie-level function as in the 
+    // case with /noNLarith.
+    public bool TranslateToFunctionCall(Expression expr) {
+      if (!(expr is BinaryExpr)) {
+        return false;
+      }
+      BinaryExpr e = (BinaryExpr) expr;
+      bool isReal = e.E0.Type.IsNumericBased(Type.NumericPersuation.Real);
+      switch (e.ResolvedOp) {
+        case BinaryExpr.ResolvedOpcode.Lt:
+        case BinaryExpr.ResolvedOpcode.Le:
+        case BinaryExpr.ResolvedOpcode.Ge:
+        case BinaryExpr.ResolvedOpcode.Gt:
+        case BinaryExpr.ResolvedOpcode.Add:
+        case BinaryExpr.ResolvedOpcode.Sub:
+        case BinaryExpr.ResolvedOpcode.Mul:
+        case BinaryExpr.ResolvedOpcode.Div:
+        case BinaryExpr.ResolvedOpcode.Mod:
+          if (!isReal && DafnyOptions.O.DisableNLarith) {
+            return true;
+          }
+          break;
+      }
+      return false;
+    }
     private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) {
       bool expr_is_killer = false;
       var new_expr = TriggerUtils.MaybeWrapInOld(TriggerUtils.PrepareExprForInclusionInTrigger(expr, out expr_is_killer), cache.exprsInOldContext.Contains(expr));
diff --git a/Test/dafny4/Bug124.dfy b/Test/dafny4/Bug124.dfy
new file mode 100644
index 00000000..60f26a00
--- /dev/null
+++ b/Test/dafny4/Bug124.dfy
@@ -0,0 +1,14 @@
+// RUN: %dafny /compile:0 /autoTriggers:1 /noNLarith  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function power(n:nat, e:nat) : int
+
+lemma lemma_power()
+    ensures forall n:nat, e:nat :: 0 <= n * e && power(n, e) == 5;
+{
+    forall n:nat, e:nat 
+        ensures 0 <= n * e && power(n, e) == 5;
+    {
+        assume false;
+    }
+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug124.dfy.expect b/Test/dafny4/Bug124.dfy.expect
new file mode 100644
index 00000000..52595bf9
--- /dev/null
+++ b/Test/dafny4/Bug124.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
-- 
cgit v1.2.3