diff --git a/svcomp/normalize.sh b/svcomp/normalize.sh
index 2e3fc89fa691e14043841e38edc7c450a67872cf..a88e78488e491cd4c5ae1d67abb401fe93bd49bf 100755
--- a/svcomp/normalize.sh
+++ b/svcomp/normalize.sh
@@ -11,3 +11,8 @@ sed -i 's/__VERIFIER_nondet_uchar()/Frama_C_interval(0, UCHAR_MAX)/g' $*
sed -i 's/__VERIFIER_nondet_char()/Frama_C_interval(CHAR_MIN, CHAR_MAX)/g' $*
sed -i 's/__VERIFIER_nondet_ulong()/Frama_C_unsigned_long_interval(0, ULONG_MAX)/g' $*
+sed -i 's/extern int Frama_C_interval(INT_MIN, INT_MAX);//g' $*
+sed -i 's/extern short Frama_C_interval(SHRT_MIN, SHRT_MAX);//g' $*
+sed -i 's/extern unsigned chard Frama_C_interval(0, UCHAR_MAX);//g' $*
+sed -i 's/extern char Frama_C_interval(CHAR_MIN, CHAR_MAX);//g' $*
+sed -i 's/exterm unsigned long Frama_C_unsigned_long_interval(0, ULONG_MAX);//g' $*
diff --git a/svcomp/reducercommutativity/.frama-c/GNUmakefile b/svcomp/reducercommutativity/.frama-c/GNUmakefile
new file mode 100644
index 0000000000000000000000000000000000000000..9bbcdbac53026aa67f2332bc62c99a0d4ce11c3c
--- /dev/null
+++ b/svcomp/reducercommutativity/.frama-c/GNUmakefile
@@ -0,0 +1,69 @@
+# Makefile template for Frama-C/Eva case studies.
+# For details and usage information, see the Frama-C User Manual.
+
+### Prologue. Do not modify this block. #######################################
+-include path.mk
+FRAMAC ?= frama-c
+include $(shell $(FRAMAC)-config -scripts)/prologue.mk
+###############################################################################
+
+# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
+
+MACHDEP = x86_32
+
+## Preprocessing flags (for -cpp-extra-args)
+CPPFLAGS += \
+ -D__FC_PATCHED \
+ -I../../lib \
+ -I../../../frama-c/share/libc
+
+## General flags
+FCFLAGS += \
+ -add-symbolic-path=.:..\
+ -kernel-warn-key annot:missing-spec=abort \
+ -kernel-warn-key typing:implicit-function-declaration=abort \
+ -absolute-valid-range 0x4347C000-0x4347FFFF \
+ -c11\
+
+## Eva-specific flags
+EVAFLAGS += \
+ -eva-precision 5 \
+ -eva-warn-key builtins:missing-spec=abort \
+
+## GUI-only flags
+FCGUIFLAGS += \
+ -add-symbolic-path=.:..\
+
+# exclude files with recursive functions, and those testing memory leaks
+filter-out-substring = $(foreach v,$(2),$(if $(findstring $(1),$(v)),,$(v)))
+SRCS:=$(sort $(wildcard ../*.c))
+
+# [target] converts a file name into a suitable target name,
+# removing the initial '../', the final '.c'.
+target = $(subst /,/,$(patsubst %.c,%,$(1:../%=%)))
+
+EVA_TARGETS:=$(foreach s,$(SRCS),$(call target,$(s)).eva)
+TARGETS:=$(EVA_TARGETS)
+
+### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
+define generate-parse-rules =
+$(call target,$(1)).parse: $(if $(findstring cross_file,$(1)),,) $(1)
+$(call target,$(1)).parse: SRCS += ../../../frama-c/share/libc/__fc_builtin.c
+
+$(call target,$(1)).eva/eval.txt: $(call target, $(1)).eva
+ ./evaluate_case.sh $(subst .c,,$(1)).yml $$</alarms.csv $$</nonterm.log > $$</eval.txt
+endef
+$(foreach s,$(SRCS),$(eval $(call generate-parse-rules,$(s))))
+
+eval_summary.txt: $(addsuffix /eval.txt, $(TARGETS))
+ cat $^ > eval_summary.txt
+
+evaluate: eval_summary.txt
+.PHONY: eval_summary.txt
+
+fclean: clean
+ rm eval_summary.txt
+
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+###############################################################################
diff --git a/svcomp/reducercommutativity/.frama-c/eval_summary.txt b/svcomp/reducercommutativity/.frama-c/eval_summary.txt
new file mode 100644
index 0000000000000000000000000000000000000000..97b24a7ca434b210ae372e8f0b2c351587e82b46
--- /dev/null
+++ b/svcomp/reducercommutativity/.frama-c/eval_summary.txt
@@ -0,0 +1,242 @@
+
+Termination spec: true
+avg.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+avg.eva/alarms.csv (true): Imprecise
+__________________________________
+
+Termination spec: true
+avg05-1.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+avg05-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+avg05-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Defined Behavior spec: false
+avg10-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Termination spec: true
+avg10-2.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+avg10-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+avg20-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+avg20-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+avg40-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+avg40-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Unreachability spec: true
+avg60-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+avg60-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Termination spec: true
+max.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+max.eva/alarms.csv (true): Imprecise
+__________________________________
+
+Termination spec: true
+max05-1.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+max05-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+max05-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Termination spec: true
+max10-1.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+max10-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+max10-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+max20-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+max20-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+max40-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+max40-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Defined Behavior spec: false
+max60-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+max60-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Termination spec: true
+rangesum.eva/alarms.csv (true): Valid
+
+Unreachability spec: false
+rangesum.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Termination spec: true
+rangesum05.eva/alarms.csv (true): Valid
+
+Unreachability spec: false
+rangesum05.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Termination spec: true
+rangesum10.eva/alarms.csv (true): Valid
+
+Unreachability spec: false
+rangesum10.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Unreachability spec: false
+rangesum20.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Unreachability spec: false
+rangesum40.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Unreachability spec: false
+rangesum60.eva/alarms.csv (false): Imprecise
+__________________________________
+
+Termination spec: true
+sep.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+sep.eva/alarms.csv (true): Imprecise
+__________________________________
+
+Termination spec: true
+sep05-1.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+sep05-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sep05-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Defined Behavior spec: false
+sep10-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sep10-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Unreachability spec: true
+sep20-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sep20-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sep40-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sep40-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Defined Behavior spec: false
+sep60-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sep60-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Termination spec: true
+sum.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+sum.eva/alarms.csv (true): Imprecise
+__________________________________
+
+Defined Behavior spec: false
+sum05-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Termination spec: true
+sum05-2.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+sum05-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Termination spec: true
+sum10-1.eva/alarms.csv (true): Valid
+
+Unreachability spec: true
+sum10-1.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sum10-2.eva/alarms.csv (false): Valid
+__________________________________
+
+Defined Behavior spec: false
+sum20-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sum20-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sum40-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sum40-2.eva/alarms.csv (true): Valid
+__________________________________
+
+Defined Behavior spec: false
+sum60-1.eva/alarms.csv (false): Valid
+__________________________________
+
+Unreachability spec: true
+sum60-2.eva/alarms.csv (true): Valid
+__________________________________
diff --git a/svcomp/reducercommutativity/.frama-c/evaluate_case.sh b/svcomp/reducercommutativity/.frama-c/evaluate_case.sh
new file mode 100755
index 0000000000000000000000000000000000000000..f6e23d8d06df40857ffedf4bf69bf81af5fa253c
--- /dev/null
+++ b/svcomp/reducercommutativity/.frama-c/evaluate_case.sh
@@ -0,0 +1,129 @@
+#!/bin/bash -u
+
+# Script is not yet complete and shouldn't yet be used
+# https://sv-comp.sosy-lab.org/2020/rules.php
+# to check the meaning of all specs in *.yml files
+
+if [ $# -lt 2 ]; then
+ echo "usage: $0 (dotyml_file_spec) path/to/alarms.csv path/to/nonterm.log"
+ exit 1
+fi
+
+#set argument variables
+dotyml="$1"
+alarmcsv="$2"
+nontermlog="$3"
+
+#get number of lines in FramaC's target alarm.csv file
+alarms=$(wc -l $alarmcsv | cut -d' ' -f1)
+
+#check and get FramaC's conclusion
+valid_deref=$(grep "index_bound" $alarmcsv)
+if [ -z "$valid_deref" ]; then
+ valid_deref=$(grep "mem_access" $alarmcsv)
+fi
+
+#check number of lines in target's nonterm.log
+nonterm=$(wc -l $nontermlog | cut -d' ' -f1)
+
+#check and get spec true/false
+termination=$(grep "property_file: ../properties/termination.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
+
+#check and get spec true/false
+memsafety=$(grep "property_file: ../properties/valid-memsafety.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
+
+#check and get spec true/false
+defbehavior=$(grep "property_file: ../properties/def-behavior.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
+
+#check and get spec true/false
+unreachability=$(grep "property_file: ../properties/unreach-call.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
+
+## This part is suppose to establish if program must terminate.
+# if $termination = true then it must terminate one way or another, call to abort is accepted
+# else if $termination = false, then program is most likely an infinite loop and must not exit by ordinary means, ie should be interrupted
+#
+# NO FALSE CASE IN ARRAY-EXAMPLES
+if [ -n "$termination" ]; then
+ printf "\nTermination spec: $termination\n"
+ case $termination in
+ "true")
+ if [ "$nonterm" -ge 0 ]; then
+ echo "$2 ($termination): Valid"
+ else
+ echo "$2 ($termination): Imprecise"
+ fi
+ ;;
+ *)
+ printf "An error occured in termination :C.\n"
+ exit 1
+ esac
+fi
+
+## This part is suppose to establish whether the error function __VERIFIER_error() was reached during a finite execution of the program.
+#
+# if $unreachability = true, then given function must never be reached in any path of the execution.
+# else if $unreachability = false, then given __VERIFIER_error() function must be reached at some point of the program, and program must exit by a call to the abort(); function.
+#
+#
+if [ -n "$unreachability" ]; then
+ printf "\nUnreachability spec: $unreachability\n"
+ case $unreachability in
+ "true")
+ if [ "$nonterm" -eq 0 ]; then
+ echo "$2 ($unreachability): Valid"
+ else
+ echo "$2 ($unreachability): Imprecise"
+ fi
+ ;;
+ "false")
+ if [ "$nonterm" -ne 0 ]; then
+ echo "$2 ($unreachability): Valid"
+ else
+ echo "$2 ($unreachability): Imprecise"
+ fi
+ ;;
+ *)
+ printf "An error occured in unreachability :C.\n"
+ exit 1
+ esac
+fi
+
+## This part tends to adress the memsafety spec. To verify a set of subspec found in all targets.yml files
+#
+# The only memsafety subspec present in ARRAY-EXAMPLES is VALID-DEREF. Therefore it's the only one this script checks
+#
+#FALSE case is omitted because of its absence in ARRAY-EXAMPLES
+if [ -n "$memsafety" ]; then
+ printf "\nValid-Memsafety spec: $memsafety\n"
+ case $memsafety in
+ "false")
+ if [ -n "$valid_deref" ]; then
+ echo "$2 ($memsafety): Valid"
+ else
+ echo "$2 ($memsafety): Imprecise"
+ fi
+ ;;
+ *)
+ printf "An error occured in memsafety :C.\n"
+ exit 1
+ esac
+fi
+
+## This part tends to handle the one and only case of Def-behaviour spec.
+# it is FALSE and is found in standard_find_ground-2.yml and standard_sentinel-1.yml
+if [ -n "$defbehavior" ]; then
+ printf "\nDefined Behavior spec: $defbehavior\n"
+ case $defbehavior in
+ "false")
+ if [ "$alarms" -ne 0 ]; then
+ echo "$2 ($defbehavior): Valid"
+ else
+ echo "$2 ($defbehavior): Imprecise"
+ fi
+ ;;
+ *)
+ printf "An error occured in defbehavior :C.\n"
+ exit 1
+ esac
+fi
+echo "__________________________________"
diff --git a/svcomp/reducercommutativity/.frama-c/path.mk b/svcomp/reducercommutativity/.frama-c/path.mk
new file mode 120000
index 0000000000000000000000000000000000000000..261a4f4b4e777fcdc5f492ab77b0b68118ebffca
--- /dev/null
+++ b/svcomp/reducercommutativity/.frama-c/path.mk
@@ -0,0 +1 @@
+../frama-c-cgc-path.mk
\ No newline at end of file
diff --git a/svcomp/reducercommutativity/LICENSE.txt b/svcomp/reducercommutativity/LICENSE.txt
new file mode 100644
index 0000000000000000000000000000000000000000..ebbd4f95cfb0e4c7b32898404beb928b2c91192e
--- /dev/null
+++ b/svcomp/reducercommutativity/LICENSE.txt
@@ -0,0 +1,23 @@
+Copyright (c) 2015, Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+ * Redistributions of source code must retain the above copyright notice,
+ this list of conditions and the following disclaimer.
+ * Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGE.
\ No newline at end of file
diff --git a/svcomp/reducercommutativity/Makefile b/svcomp/reducercommutativity/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..49b2905c19f549ad36f2faa0a7c30c8e219b8db4
--- /dev/null
+++ b/svcomp/reducercommutativity/Makefile
@@ -0,0 +1,3 @@
+LEVEL := ../
+
+include $(LEVEL)/Makefile.config
diff --git a/svcomp/reducercommutativity/README.txt b/svcomp/reducercommutativity/README.txt
new file mode 100644
index 0000000000000000000000000000000000000000..0093aafbf10e56c961e5aab0326f4448e50b01b4
--- /dev/null
+++ b/svcomp/reducercommutativity/README.txt
@@ -0,0 +1,12 @@
+Benchmarks used in the paper "Commutativity of Reducers"
+which was published at TACAS 2015 and
+written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+
+We checks if a function is "deterministic" w.r.t. all possible permutations
+of an input array. Such property is desirable for reducers in the
+map-reduce programming model. It ensures that the program always computes
+the same results on the same input data set.
+
+Submitted by Matthias Heizmann.
+
diff --git a/svcomp/reducercommutativity/avg.c b/svcomp/reducercommutativity/avg.c
new file mode 100644
index 0000000000000000000000000000000000000000..4633c5503f826a8fc1fd0b40b22b3523f8912661
--- /dev/null
+++ b/svcomp/reducercommutativity/avg.c
@@ -0,0 +1,58 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define fun avg
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ N = Frama_C_interval(INT_MIN, INT_MAX);
+ if (N > 1) {
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg.yml b/svcomp/reducercommutativity/avg.yml
new file mode 100644
index 0000000000000000000000000000000000000000..8ca5b57abba245151494698a6d8a09058a750fff
--- /dev/null
+++ b/svcomp/reducercommutativity/avg.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: avg_true-unreach-call_true-termination.i
+input_files: 'avg.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg05-1.c b/svcomp/reducercommutativity/avg05-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..f0d890c517588aa62feb6039c6a51f6f5543dc5e
--- /dev/null
+++ b/svcomp/reducercommutativity/avg05-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg05-1.yml b/svcomp/reducercommutativity/avg05-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..6662db49c6f24b38c67f1e8a58f246fae2749146
--- /dev/null
+++ b/svcomp/reducercommutativity/avg05-1.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: avg05_true-unreach-call_true-termination.i
+input_files: 'avg05-1.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg05-2.c b/svcomp/reducercommutativity/avg05-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..b575df0048715a23dd101bcdb5729ee00c6ee388
--- /dev/null
+++ b/svcomp/reducercommutativity/avg05-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg05-2.yml b/svcomp/reducercommutativity/avg05-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..916247cbb0182652873a5cbbec4b5691be374971
--- /dev/null
+++ b/svcomp/reducercommutativity/avg05-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: avg05_false-def-behavior.i
+input_files: 'avg05-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/avg10-1.c b/svcomp/reducercommutativity/avg10-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..9caa88d882375a507ac894de65a2c16c7ade1f6f
--- /dev/null
+++ b/svcomp/reducercommutativity/avg10-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg10-1.yml b/svcomp/reducercommutativity/avg10-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..0e3fd1467974672a219aa246de29bb9cf996b87b
--- /dev/null
+++ b/svcomp/reducercommutativity/avg10-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: avg10_false-def-behavior.i
+input_files: 'avg10-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/avg10-2.c b/svcomp/reducercommutativity/avg10-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..63229ae34bf7525978581f3b3863932f7645c1ba
--- /dev/null
+++ b/svcomp/reducercommutativity/avg10-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg10-2.yml b/svcomp/reducercommutativity/avg10-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..61e0cbb6c8fb633cc95bf45fd976419b3bb0bb6a
--- /dev/null
+++ b/svcomp/reducercommutativity/avg10-2.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: avg10_true-unreach-call_true-termination.i
+input_files: 'avg10-2.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg20-1.c b/svcomp/reducercommutativity/avg20-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..a47d3434eaf40938fe7746bc71858056e5f66998
--- /dev/null
+++ b/svcomp/reducercommutativity/avg20-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg20-1.yml b/svcomp/reducercommutativity/avg20-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..ca77fdc5650b09fc027c667e53bf127c3ab6753f
--- /dev/null
+++ b/svcomp/reducercommutativity/avg20-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: avg20_false-def-behavior.i
+input_files: 'avg20-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/avg20-2.c b/svcomp/reducercommutativity/avg20-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..7eaf13c035ccd35ce0725b89117150638e95c513
--- /dev/null
+++ b/svcomp/reducercommutativity/avg20-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg20-2.yml b/svcomp/reducercommutativity/avg20-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..89db14bbc2979ef4641a9c16cf3625520d432dd4
--- /dev/null
+++ b/svcomp/reducercommutativity/avg20-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: avg20_true-unreach-call.i
+input_files: 'avg20-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg40-1.c b/svcomp/reducercommutativity/avg40-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..1125af7f29cda403484922984f35117b6506e5ff
--- /dev/null
+++ b/svcomp/reducercommutativity/avg40-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg40-1.yml b/svcomp/reducercommutativity/avg40-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..32cb868c8babba2ab7343d8a86bcd468e0600ac8
--- /dev/null
+++ b/svcomp/reducercommutativity/avg40-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: avg40_false-def-behavior.i
+input_files: 'avg40-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/avg40-2.c b/svcomp/reducercommutativity/avg40-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..c3169c537b904d5d1bc9dd5eea723d469867a2a5
--- /dev/null
+++ b/svcomp/reducercommutativity/avg40-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg40-2.yml b/svcomp/reducercommutativity/avg40-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..8687001ea3a204053cd4cfcabdc1934daab9cd9e
--- /dev/null
+++ b/svcomp/reducercommutativity/avg40-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: avg40_true-unreach-call.i
+input_files: 'avg40-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg60-1.c b/svcomp/reducercommutativity/avg60-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..48aa6b8580a6c6d5cb0c9f75a69040e46480b88d
--- /dev/null
+++ b/svcomp/reducercommutativity/avg60-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg60-1.yml b/svcomp/reducercommutativity/avg60-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..a80991cc7e61f36f68bd43e648b9efc755ccbba1
--- /dev/null
+++ b/svcomp/reducercommutativity/avg60-1.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: avg60_true-unreach-call.i
+input_files: 'avg60-1.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/avg60-2.c b/svcomp/reducercommutativity/avg60-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..8f566d3e2563315219fb1ef9254a83a4b5ff5d58
--- /dev/null
+++ b/svcomp/reducercommutativity/avg60-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun avg
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int avg (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret / N;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/avg60-2.yml b/svcomp/reducercommutativity/avg60-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..891f7539c84f8f40eb77dc2643c4f1903dc06915
--- /dev/null
+++ b/svcomp/reducercommutativity/avg60-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: avg60_false-def-behavior.i
+input_files: 'avg60-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/frama-c-cgc-path.mk b/svcomp/reducercommutativity/frama-c-cgc-path.mk
new file mode 100644
index 0000000000000000000000000000000000000000..f6e877ad3e205a7856ffefe98c7993c570563e3a
--- /dev/null
+++ b/svcomp/reducercommutativity/frama-c-cgc-path.mk
@@ -0,0 +1,8 @@
+FRAMAC_DIR=../../../frama-c/build/bin
+ifeq ($(wildcard $(FRAMAC_DIR)),)
+# Frama-C not installed locally; using the version in the PATH
+else
+FRAMAC=$(FRAMAC_DIR)/frama-c
+FRAMAC_GUI=$(FRAMAC_DIR)/frama-c-gui
+FRAMAC_CONFIG=$(FRAMAC_DIR)/frama-c-config
+endif
diff --git a/svcomp/reducercommutativity/max.c b/svcomp/reducercommutativity/max.c
new file mode 100644
index 0000000000000000000000000000000000000000..21e1400c8be2c50afcc5e34eebd632692c811dd4
--- /dev/null
+++ b/svcomp/reducercommutativity/max.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ N = Frama_C_interval(INT_MIN, INT_MAX);
+ if (N > 1) {
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max.yml b/svcomp/reducercommutativity/max.yml
new file mode 100644
index 0000000000000000000000000000000000000000..4b4bfd108f9f85fa0f28e22ac9481c9009a4586e
--- /dev/null
+++ b/svcomp/reducercommutativity/max.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: max_true-unreach-call_true-termination.i
+input_files: 'max.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/max05-1.c b/svcomp/reducercommutativity/max05-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..ba4b6ad0bcbfd87c6423b83b349fcbebbfcdacc6
--- /dev/null
+++ b/svcomp/reducercommutativity/max05-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max05-1.yml b/svcomp/reducercommutativity/max05-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..c2335acf3000d643ad454fa216b11d75dddc7def
--- /dev/null
+++ b/svcomp/reducercommutativity/max05-1.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: max05_true-unreach-call_true-termination.i
+input_files: 'max05-1.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/max05-2.c b/svcomp/reducercommutativity/max05-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..31f4b9dbb53fb234a69101ad40981876870afc60
--- /dev/null
+++ b/svcomp/reducercommutativity/max05-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max05-2.yml b/svcomp/reducercommutativity/max05-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..c0614d6aefd9a68fdcb55b8fcc79c2899d3956bb
--- /dev/null
+++ b/svcomp/reducercommutativity/max05-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: max05_false-def-behavior.i
+input_files: 'max05-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/max10-1.c b/svcomp/reducercommutativity/max10-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..2a6d751c07dacb268ab8fc7520396e364d853a69
--- /dev/null
+++ b/svcomp/reducercommutativity/max10-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max10-1.yml b/svcomp/reducercommutativity/max10-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..8a7cd3f1c419db363a2357efe011193b55cab689
--- /dev/null
+++ b/svcomp/reducercommutativity/max10-1.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: max10_true-unreach-call_true-termination.i
+input_files: 'max10-1.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/max10-2.c b/svcomp/reducercommutativity/max10-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..e37284a12589b16673359fa9612f53fd1d12e92d
--- /dev/null
+++ b/svcomp/reducercommutativity/max10-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max10-2.yml b/svcomp/reducercommutativity/max10-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..702485612eb99b46f0b23c6125018dae88e68d20
--- /dev/null
+++ b/svcomp/reducercommutativity/max10-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: max10_false-def-behavior.i
+input_files: 'max10-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/max20-1.c b/svcomp/reducercommutativity/max20-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..4cb0ef709208bdd327c1184e1c63c78c6abb26c2
--- /dev/null
+++ b/svcomp/reducercommutativity/max20-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max20-1.yml b/svcomp/reducercommutativity/max20-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..439cc7ae6313485a69c276d34d68e059012d57f2
--- /dev/null
+++ b/svcomp/reducercommutativity/max20-1.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: max20_true-unreach-call.i
+input_files: 'max20-1.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/max20-2.c b/svcomp/reducercommutativity/max20-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..ab4a9199e7c775c7e702f78b5ea9bd6354c8a5a3
--- /dev/null
+++ b/svcomp/reducercommutativity/max20-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max20-2.yml b/svcomp/reducercommutativity/max20-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..a20610d973df73c6ab49cbc974f7d519ae3e86ba
--- /dev/null
+++ b/svcomp/reducercommutativity/max20-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: max20_false-def-behavior.i
+input_files: 'max20-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/max40-1.c b/svcomp/reducercommutativity/max40-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..631e18b11d8e93cfec4817bff28627e3bdb721f1
--- /dev/null
+++ b/svcomp/reducercommutativity/max40-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max40-1.yml b/svcomp/reducercommutativity/max40-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..f6cc70bd17be6de7bc352d9476687a1682a0f878
--- /dev/null
+++ b/svcomp/reducercommutativity/max40-1.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: max40_true-unreach-call.i
+input_files: 'max40-1.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/max40-2.c b/svcomp/reducercommutativity/max40-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..a7c688698e36768dc1cdf1ba0d21df5409ee736b
--- /dev/null
+++ b/svcomp/reducercommutativity/max40-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max40-2.yml b/svcomp/reducercommutativity/max40-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..f7f67210f1e00a2ba8a3ddd5652774cd5ac97e80
--- /dev/null
+++ b/svcomp/reducercommutativity/max40-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: max40_false-def-behavior.i
+input_files: 'max40-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/max60-1.c b/svcomp/reducercommutativity/max60-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..4f80338b9a41f7f1c3c1ecdbd81e49196214deff
--- /dev/null
+++ b/svcomp/reducercommutativity/max60-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max60-1.yml b/svcomp/reducercommutativity/max60-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..096f1f776b675aad013791e82037e3875d59526a
--- /dev/null
+++ b/svcomp/reducercommutativity/max60-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: max60_false-def-behavior.i
+input_files: 'max60-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/max60-2.c b/svcomp/reducercommutativity/max60-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..53bb33ca4104b800f212f5b86a7905031a5e4a52
--- /dev/null
+++ b/svcomp/reducercommutativity/max60-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun max
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int max (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret < x[i] ? x[i] : ret;
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/max60-2.yml b/svcomp/reducercommutativity/max60-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..d1a7b0d8294af9b733e090bbc2a7609b43f260d7
--- /dev/null
+++ b/svcomp/reducercommutativity/max60-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: max60_true-unreach-call.i
+input_files: 'max60-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum.c b/svcomp/reducercommutativity/rangesum.c
new file mode 100644
index 0000000000000000000000000000000000000000..7215e5209db4da7febde41c3bac0cf66e5999df7
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum.c
@@ -0,0 +1,74 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ N = Frama_C_interval(INT_MIN, INT_MAX);
+ if (N > 1) {
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum.yml b/svcomp/reducercommutativity/rangesum.yml
new file mode 100644
index 0000000000000000000000000000000000000000..92285eca825ea60e17a7c6cecb7ece06fa450dd9
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum.yml
@@ -0,0 +1,14 @@
+format_version: '1.0'
+
+# old file name: rangesum_false-unreach-call_true-termination.i
+input_files: 'rangesum.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum05.c b/svcomp/reducercommutativity/rangesum05.c
new file mode 100644
index 0000000000000000000000000000000000000000..2a93ec2c9a8db6535679cb958e3858fe4f00cb04
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum05.c
@@ -0,0 +1,70 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum05.yml b/svcomp/reducercommutativity/rangesum05.yml
new file mode 100644
index 0000000000000000000000000000000000000000..cab42acc834ee76220772ffba791cc6941f3c6f3
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum05.yml
@@ -0,0 +1,14 @@
+format_version: '1.0'
+
+# old file name: rangesum05_false-unreach-call_true-termination.i
+input_files: 'rangesum05.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum10.c b/svcomp/reducercommutativity/rangesum10.c
new file mode 100644
index 0000000000000000000000000000000000000000..c30189bd80e0586b559e9bb66e2c94062771eae7
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum10.c
@@ -0,0 +1,70 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum10.yml b/svcomp/reducercommutativity/rangesum10.yml
new file mode 100644
index 0000000000000000000000000000000000000000..eff52436d5a69485b0a90473fc286adf9e3a0b08
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum10.yml
@@ -0,0 +1,14 @@
+format_version: '1.0'
+
+# old file name: rangesum10_false-unreach-call_true-termination.i
+input_files: 'rangesum10.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum20.c b/svcomp/reducercommutativity/rangesum20.c
new file mode 100644
index 0000000000000000000000000000000000000000..db062633fa27141ca571647557906776bb388b3f
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum20.c
@@ -0,0 +1,70 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum20.yml b/svcomp/reducercommutativity/rangesum20.yml
new file mode 100644
index 0000000000000000000000000000000000000000..7abccd97829aa51c2b0f7facbdc7908697903580
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum20.yml
@@ -0,0 +1,12 @@
+format_version: '1.0'
+
+# old file name: rangesum20_false-unreach-call.i
+input_files: 'rangesum20.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum40.c b/svcomp/reducercommutativity/rangesum40.c
new file mode 100644
index 0000000000000000000000000000000000000000..3525a4ece94fb0c5f1d496bf876a0f6a4c69fbc0
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum40.c
@@ -0,0 +1,70 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum40.yml b/svcomp/reducercommutativity/rangesum40.yml
new file mode 100644
index 0000000000000000000000000000000000000000..e675584cf3e5d3c7ac7f631cc577bdb2d2ea2340
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum40.yml
@@ -0,0 +1,12 @@
+format_version: '1.0'
+
+# old file name: rangesum40_false-unreach-call.i
+input_files: 'rangesum40.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/rangesum60.c b/svcomp/reducercommutativity/rangesum60.c
new file mode 100644
index 0000000000000000000000000000000000000000..97b9d4b8624236ab79b955d2c94a6747db3a328b
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum60.c
@@ -0,0 +1,70 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun rangesum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+void init_nondet(int x[N]) {
+ int i;
+ for (i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+}
+
+int rangesum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ int cnt = 0;
+ for (i = 0; i < N; i++) {
+ if( i > N/2){
+ ret = ret + x[i];
+ cnt = cnt + 1;
+ }
+ }
+ if ( cnt !=0)
+ return ret / cnt;
+ else
+ return 0;
+}
+
+int main ()
+{
+ int x[N];
+ init_nondet(x);
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/rangesum60.yml b/svcomp/reducercommutativity/rangesum60.yml
new file mode 100644
index 0000000000000000000000000000000000000000..040d9eda1f9953523d661bb3c798996e083f4bd4
--- /dev/null
+++ b/svcomp/reducercommutativity/rangesum60.yml
@@ -0,0 +1,12 @@
+format_version: '1.0'
+
+# old file name: rangesum60_false-unreach-call.i
+input_files: 'rangesum60.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: false
+ - property_file: ../properties/coverage-error-call.prp
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep.c b/svcomp/reducercommutativity/sep.c
new file mode 100644
index 0000000000000000000000000000000000000000..f446127a38526cad5d58e5c52bfccfaf060b1fc2
--- /dev/null
+++ b/svcomp/reducercommutativity/sep.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ N = Frama_C_interval(INT_MIN, INT_MAX);
+ if (N > 1) {
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep.yml b/svcomp/reducercommutativity/sep.yml
new file mode 100644
index 0000000000000000000000000000000000000000..dcb748a75a5d807eb1f710e73375fae1331a1334
--- /dev/null
+++ b/svcomp/reducercommutativity/sep.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: sep_true-unreach-call_true-termination.i
+input_files: 'sep.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep05-1.c b/svcomp/reducercommutativity/sep05-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..d1ffcf4e4a212ebd93d3b19a352d6c2eef48d051
--- /dev/null
+++ b/svcomp/reducercommutativity/sep05-1.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep05-1.yml b/svcomp/reducercommutativity/sep05-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..2b4ad690a946c2be8b4b9bd84ea4848082d444c7
--- /dev/null
+++ b/svcomp/reducercommutativity/sep05-1.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: sep05_true-unreach-call_true-termination.i
+input_files: 'sep05-1.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep05-2.c b/svcomp/reducercommutativity/sep05-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..747308e07c125a9dc649ff5766c98578ad46e065
--- /dev/null
+++ b/svcomp/reducercommutativity/sep05-2.c
@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep05-2.yml b/svcomp/reducercommutativity/sep05-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..af8f4428b5cdd79c6716c129aade96d4b12defe2
--- /dev/null
+++ b/svcomp/reducercommutativity/sep05-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sep05_false-def-behavior.i
+input_files: 'sep05-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sep10-1.c b/svcomp/reducercommutativity/sep10-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..9754abe1d01a1d68cdf07fa2445629f1985dea7a
--- /dev/null
+++ b/svcomp/reducercommutativity/sep10-1.c
@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep10-1.yml b/svcomp/reducercommutativity/sep10-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..950f400851a7947367660cf54fea1493b4e400e2
--- /dev/null
+++ b/svcomp/reducercommutativity/sep10-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sep10_false-def-behavior.i
+input_files: 'sep10-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sep10-2.c b/svcomp/reducercommutativity/sep10-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..357be51a444232f069f7688417aa03119fc6cdaa
--- /dev/null
+++ b/svcomp/reducercommutativity/sep10-2.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep10-2.yml b/svcomp/reducercommutativity/sep10-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..b990fbf8cebcd34931fbfa8fb5c7e8de8deccd8b
--- /dev/null
+++ b/svcomp/reducercommutativity/sep10-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sep10_true-unreach-call.i
+input_files: 'sep10-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep20-1.c b/svcomp/reducercommutativity/sep20-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..9fb6dd3ac5da6a176a226c43b797e3ec8d8baf94
--- /dev/null
+++ b/svcomp/reducercommutativity/sep20-1.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep20-1.yml b/svcomp/reducercommutativity/sep20-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..8e524c46bea3e85b7eb25c0a18c504ee228c95f6
--- /dev/null
+++ b/svcomp/reducercommutativity/sep20-1.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sep20_true-unreach-call.i
+input_files: 'sep20-1.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep20-2.c b/svcomp/reducercommutativity/sep20-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..7cefca3ab3c2c48e3825aa16315f5564386cd6a8
--- /dev/null
+++ b/svcomp/reducercommutativity/sep20-2.c
@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep20-2.yml b/svcomp/reducercommutativity/sep20-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..94cbd8da58a5bbc0efce2e5126b92e3ce565c7d6
--- /dev/null
+++ b/svcomp/reducercommutativity/sep20-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sep20_false-def-behavior.i
+input_files: 'sep20-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sep40-1.c b/svcomp/reducercommutativity/sep40-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..20d19051114921f76633154ddc00473937fac29b
--- /dev/null
+++ b/svcomp/reducercommutativity/sep40-1.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep40-1.yml b/svcomp/reducercommutativity/sep40-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..e786d0df4c155483dee467dfbbfd3d66345a91fe
--- /dev/null
+++ b/svcomp/reducercommutativity/sep40-1.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sep40_true-unreach-call.i
+input_files: 'sep40-1.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sep40-2.c b/svcomp/reducercommutativity/sep40-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..6375eaa833d8221db40d6db5a9241d47c5ad35ce
--- /dev/null
+++ b/svcomp/reducercommutativity/sep40-2.c
@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep40-2.yml b/svcomp/reducercommutativity/sep40-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..2fb3809b970e24f535c8b8fca334cd3f65b2b39f
--- /dev/null
+++ b/svcomp/reducercommutativity/sep40-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sep40_false-def-behavior.i
+input_files: 'sep40-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sep60-1.c b/svcomp/reducercommutativity/sep60-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..588bf810c7adaa381d64ecadb9b2e838db7b36f7
--- /dev/null
+++ b/svcomp/reducercommutativity/sep60-1.c
@@ -0,0 +1,57 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep60-1.yml b/svcomp/reducercommutativity/sep60-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..022e141c81077ae38badaa1b360f4793b3179675
--- /dev/null
+++ b/svcomp/reducercommutativity/sep60-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sep60_false-def-behavior.i
+input_files: 'sep60-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sep60-2.c b/svcomp/reducercommutativity/sep60-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..9c4fd1b59ceb4fdec8185e046a04cec2afd35cf6
--- /dev/null
+++ b/svcomp/reducercommutativity/sep60-2.c
@@ -0,0 +1,62 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun sep
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sep (int x[N])
+{
+ long long ret =0;
+ for(int i=0;i<N;i++)
+ {
+ if(x[i]%2==0)
+ ret++;
+ else
+ ret--;
+ }
+ return ret;
+}
+
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sep60-2.yml b/svcomp/reducercommutativity/sep60-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..2d2f6ea7f1dafbb2f6eb3dfcb59d07377b8dbf54
--- /dev/null
+++ b/svcomp/reducercommutativity/sep60-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sep60_true-unreach-call.i
+input_files: 'sep60-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum.c b/svcomp/reducercommutativity/sum.c
new file mode 100644
index 0000000000000000000000000000000000000000..ffc23ea3baf8aa8856fc115adb7c1b54408a192a
--- /dev/null
+++ b/svcomp/reducercommutativity/sum.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ N = Frama_C_interval(INT_MIN, INT_MAX);
+ if (N > 1) {
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum.yml b/svcomp/reducercommutativity/sum.yml
new file mode 100644
index 0000000000000000000000000000000000000000..c5c94860f249d6600d827063937a8f44ac0b842a
--- /dev/null
+++ b/svcomp/reducercommutativity/sum.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: sum_true-unreach-call_true-termination.i
+input_files: 'sum.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum05-1.c b/svcomp/reducercommutativity/sum05-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..501a6d31f9e19c5f3a341dab7b9fd95f14d8922e
--- /dev/null
+++ b/svcomp/reducercommutativity/sum05-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum05-1.yml b/svcomp/reducercommutativity/sum05-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..bc5f29e6c41016292c0d229c99514257d264764a
--- /dev/null
+++ b/svcomp/reducercommutativity/sum05-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sum05_false-def-behavior.i
+input_files: 'sum05-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sum05-2.c b/svcomp/reducercommutativity/sum05-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..7937bee9e29e9edb5671c8e24ea6291b523716a3
--- /dev/null
+++ b/svcomp/reducercommutativity/sum05-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 5
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum05-2.yml b/svcomp/reducercommutativity/sum05-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..344476f4d387b956f9b8c170200926925cbc8bf6
--- /dev/null
+++ b/svcomp/reducercommutativity/sum05-2.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: sum05_true-unreach-call_true-termination.i
+input_files: 'sum05-2.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum10-1.c b/svcomp/reducercommutativity/sum10-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..6e6cc0d8026b96b69cd9772996584377cf912472
--- /dev/null
+++ b/svcomp/reducercommutativity/sum10-1.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum10-1.yml b/svcomp/reducercommutativity/sum10-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..91cf625c2fc5671b5502eb7c31d4287f42aa02d3
--- /dev/null
+++ b/svcomp/reducercommutativity/sum10-1.yml
@@ -0,0 +1,13 @@
+format_version: '1.0'
+
+# old file name: sum10_true-unreach-call_true-termination.i
+input_files: 'sum10-1.i'
+
+properties:
+ - property_file: ../properties/termination.prp
+ expected_verdict: true
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum10-2.c b/svcomp/reducercommutativity/sum10-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..06941d8ef88f76c2ba84e3c154a7998f5b1576a2
--- /dev/null
+++ b/svcomp/reducercommutativity/sum10-2.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 10
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum10-2.yml b/svcomp/reducercommutativity/sum10-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..f64395959d6cda3093987c2493ced260f210f84b
--- /dev/null
+++ b/svcomp/reducercommutativity/sum10-2.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sum10_false-def-behavior.i
+input_files: 'sum10-2.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sum20-1.c b/svcomp/reducercommutativity/sum20-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..9fb3fa08ec501a361ff7109417093247b2f03d0a
--- /dev/null
+++ b/svcomp/reducercommutativity/sum20-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum20-1.yml b/svcomp/reducercommutativity/sum20-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..6945ab7786a70150099b276a91f06bf2b5364bf7
--- /dev/null
+++ b/svcomp/reducercommutativity/sum20-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sum20_false-def-behavior.i
+input_files: 'sum20-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sum20-2.c b/svcomp/reducercommutativity/sum20-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..ced6c5d1f06e1998073a403acaf434204fac6a96
--- /dev/null
+++ b/svcomp/reducercommutativity/sum20-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 20
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum20-2.yml b/svcomp/reducercommutativity/sum20-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..be488b57954ff929d9c7f86a84510cfaa1d8d70c
--- /dev/null
+++ b/svcomp/reducercommutativity/sum20-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sum20_true-unreach-call.i
+input_files: 'sum20-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum40-1.c b/svcomp/reducercommutativity/sum40-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..dccb3ed8f1a1746f692286632c009632d43d5e88
--- /dev/null
+++ b/svcomp/reducercommutativity/sum40-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum40-1.yml b/svcomp/reducercommutativity/sum40-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..8bcf00bc9d6f57933f80bdc26f6b64d83852d243
--- /dev/null
+++ b/svcomp/reducercommutativity/sum40-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sum40_false-def-behavior.i
+input_files: 'sum40-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sum40-2.c b/svcomp/reducercommutativity/sum40-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..63a47cd7cc86b97cf96b125f63c0764ef4478e0c
--- /dev/null
+++ b/svcomp/reducercommutativity/sum40-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 40
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum40-2.yml b/svcomp/reducercommutativity/sum40-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..d00fa60aa43efae1e440b12abd6ffaf6907c76ab
--- /dev/null
+++ b/svcomp/reducercommutativity/sum40-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sum40_true-unreach-call.i
+input_files: 'sum40-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp
diff --git a/svcomp/reducercommutativity/sum60-1.c b/svcomp/reducercommutativity/sum60-1.c
new file mode 100644
index 0000000000000000000000000000000000000000..8417b95a1c09d226b65e7b1b689ee8baf8e99450
--- /dev/null
+++ b/svcomp/reducercommutativity/sum60-1.c
@@ -0,0 +1,54 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum60-1.yml b/svcomp/reducercommutativity/sum60-1.yml
new file mode 100644
index 0000000000000000000000000000000000000000..d8ab00da64faaee1688c19334bbf1da9dfec8e93
--- /dev/null
+++ b/svcomp/reducercommutativity/sum60-1.yml
@@ -0,0 +1,8 @@
+format_version: '1.0'
+
+# old file name: sum60_false-def-behavior.i
+input_files: 'sum60-1.i'
+
+properties:
+ - property_file: ../properties/def-behavior.prp
+ expected_verdict: false
diff --git a/svcomp/reducercommutativity/sum60-2.c b/svcomp/reducercommutativity/sum60-2.c
new file mode 100644
index 0000000000000000000000000000000000000000..a40f4bc5b8fa645e6d7ecc6b08943279faa89633
--- /dev/null
+++ b/svcomp/reducercommutativity/sum60-2.c
@@ -0,0 +1,59 @@
+/*
+ * Benchmarks used in the paper "Commutativity of Reducers"
+ * which was published at TACAS 2015 and
+ * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
+ * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
+ *
+ * We checks if a function is "deterministic" w.r.t. all possible permutations
+ * of an input array. Such property is desirable for reducers in the
+ * map-reduce programming model. It ensures that the program always computes
+ * the same results on the same input data set.
+ */
+
+#define N 60
+#define fun sum
+
+#include "common.h"
+extern void abort(void);
+void reach_error(){}
+
+
+int sum (int x[N])
+{
+ int i;
+ long long ret;
+ ret = 0;
+ for (i = 0; i < N; i++) {
+ ret = ret + x[i];
+ }
+ return ret;
+}
+
+int main ()
+{
+ int x[N];
+ int temp;
+ int ret;
+ int ret2;
+ int ret5;
+
+ for (int i = 0; i < N; i++) {
+ x[i] = Frama_C_interval(INT_MIN, INT_MAX);
+ }
+
+ ret = fun(x);
+
+ temp=x[0];x[0] = x[1]; x[1] = temp;
+ ret2 = fun(x);
+ temp=x[0];
+ for(int i =0 ; i<N-1; i++){
+ x[i] = x[i+1];
+ }
+ x[N-1] = temp;
+ ret5 = fun(x);
+
+ if(ret != ret2 || ret !=ret5){
+ {reach_error();abort();}
+ }
+ return 1;
+}
diff --git a/svcomp/reducercommutativity/sum60-2.yml b/svcomp/reducercommutativity/sum60-2.yml
new file mode 100644
index 0000000000000000000000000000000000000000..c04773efc4e1e4e77ab3f5635bf1d4484fa9a59e
--- /dev/null
+++ b/svcomp/reducercommutativity/sum60-2.yml
@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: sum60_true-unreach-call.i
+input_files: 'sum60-2.i'
+
+properties:
+ - property_file: ../properties/unreach-call.prp
+ expected_verdict: true
+ - property_file: ../properties/coverage-branches.prp
+ - property_file: ../properties/coverage-conditions.prp
+ - property_file: ../properties/coverage-statements.prp