From 2a8c1d99675c6f588f3d2b6df0a29f1e5a1fe965 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Wed, 14 Jul 2021 14:14:58 +0200
Subject: [PATCH 1/2] Changes towards fixing summation.c

We sum with int instead of float in summation.c, since float hasn't been
support for a while. Since we only support int, casting is not
necessary. This also happens to avoid triggering some java type logic
which is interfering.
---
 examples/known-problems/summation.c                    | 10 ++++------
 .../java/vct/col/rewrite/ParallelBlockEncoder.java     |  2 +-
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/examples/known-problems/summation.c b/examples/known-problems/summation.c
index fb174de3ba..d0c8470198 100644
--- a/examples/known-problems/summation.c
+++ b/examples/known-problems/summation.c
@@ -1,13 +1,11 @@
-// -*- tab-width:2 ; indent-tabs-mode:nil -*-
 //:: cases SummationReduction
-//:: suite problem-fail
 //:: tools silicon
 //:: verdict Pass
 
-float res;
+int res;
 
 /*@
-  given seq<float> ar_values;
+  given seq<int> ar_values;
   context \pointer(ar, N, 1\2);
   context Perm(res,write);
   context ar_values == \values(ar, 0, N);
@@ -16,8 +14,8 @@ float res;
 
   ensures  res==(\sum int k ; 0 <= k && k < N ; ar_values[k] );
 @*/
-void do_sum(int N,float ar[N]){
-  res=(float)0;
+void do_sum(int N,int ar[N]){
+  res=0;
   for(int i=0;i<N;i++)
     /*@
       context ar != NULL;
diff --git a/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java b/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java
index aee97374d5..acc3adf9ef 100644
--- a/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java
+++ b/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java
@@ -745,7 +745,7 @@ private ASTNode do_block(ForEachLoop s,final boolean contract){
         body_cb.requires(create.expression(StandardOperator.PointsTo,
             copy_rw.rewrite(expr.arg(0)),
             create.reserved_name(ASTReserved.FullPerm),
-            create.expression(StandardOperator.Cast,expr.arg(0).getType(),create.constant(0))
+            create.constant(0)
         ));
       } else if(is_a_quantified(clause,Binder.Star,StandardOperator.ReducibleSum)){
         BindingExpression bclause=(BindingExpression)clause;

From 35d2c6160a349dc1ce1c649a2bbebfb1e52e98d5 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Wed, 14 Jul 2021 14:48:55 +0200
Subject: [PATCH 2/2] Move summation.c to fixed

---
 examples/known-problems/{ => fixed}/summation.c | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename examples/known-problems/{ => fixed}/summation.c (100%)

diff --git a/examples/known-problems/summation.c b/examples/known-problems/fixed/summation.c
similarity index 100%
rename from examples/known-problems/summation.c
rename to examples/known-problems/fixed/summation.c