diff --git a/tools/tacle-check/lib/tb_annotate.py b/tools/tacle-check/lib/tb_annotate.py
index 261bdcb699cf796f906c2c1c0d58e0a2f3f6a49a..3fc81020bbf9fe2a6841127e5da1297fd4ad5dd8 100644
--- a/tools/tacle-check/lib/tb_annotate.py
+++ b/tools/tacle-check/lib/tb_annotate.py
@@ -109,9 +109,9 @@ def insert_arm_mbta_brace(main_file, entry_function):
       overflow_counter++;
     }
     """)
-    
+
     prepend_to_file(main_file, '#include "core_cm0plus.h"')
-    prepend_to_file(main_file, '#include "mkl46z4.h"')
+    prepend_to_file(main_file, '#include "MKL46Z4.h"')
     prepend_to_file(main_file, '#include "slcd.h"')
 
     pre_measure = """
@@ -149,7 +149,7 @@ def insert_arm_mbta_brace(main_file, entry_function):
     }
     slcd_put_int(tmp);
     """
-    
+
     lines = []
     with open(main_file) as infile:
         for line in infile:
diff --git a/tools/tacle-check/lib/tb_wcet.py b/tools/tacle-check/lib/tb_wcet.py
index f8e998b26979a7b6b4855eb8dee621b1180ee924..4261334d8603ed0396ce1889df6ff70d02a8c70f 100644
--- a/tools/tacle-check/lib/tb_wcet.py
+++ b/tools/tacle-check/lib/tb_wcet.py
@@ -459,8 +459,9 @@ def compile_to_one_IR_file(patmos_clang, bench_files, bench_name, bench_dir, res
       filename, extension = os.path.splitext(os.path.basename(bench_file))
       tmp_file = os.path.join(result_dir, filename + "_tmp.ll")
       argv_build_tmp = [patmos_clang]
-      argv_build_tmp.extend(['-target', 'armv6m-none-eabi', '-emit-llvm', '-S', '-O2', '-o', tmp_file])
+      argv_build_tmp.extend(['-target', 'armv6m-none-eabi', '-emit-llvm', '-S', '-O3', '-o', tmp_file])
       argv_build_tmp.append('-I'+os.path.expanduser("~/neo/system/include"))
+      argv_build_tmp.append('-I'+os.path.expanduser("~/neo/system/include/MKL46Z4/include/"))
       argv_build_tmp.append('-I'+bench_dir)
       argv_build_tmp.append(bench_file)
       tmp_files.append(tmp_file)
@@ -547,35 +548,37 @@ def process_arm_benchmark(benchmark_name, files, out_dir, patmos_clang, patmos_c
         return rep;
     else:
       argv_build_ll = [patmos_clang]
-      argv_build_ll.extend(['-target', 'armv6m-none-eabi', '-O2', '-o', ll_file, '-emit-llvm', '-S'])
+      argv_build_ll.extend(['-target', 'armv6m-none-eabi', '-emit-llvm', '-S', '-O3', '-o', ll_file])
       argv_build_ll.append('-I'+os.path.expanduser("~/neo/system/include"))
+      argv_build_ll.append('-I'+os.path.expanduser("~/neo/system/include/MKL46Z4/include/"))
       argv_build_ll.append('-I'+bench_dir)
       argv_build_ll.extend(files)
 
       rep = build_with_fail_report(argv_build_ll, verbose, timeout, result_file, benchmark_name, result_dir)
       if rep is not None:
         return rep;
-    
+
     # 3.) build object file from IR file
     ofile = os.path.join(result_dir, benchmark_name + '.o')
     bench_pml = os.path.join(result_dir, benchmark_name + '.pml')
     argv = [patmos_clang]
-    argv.extend(['-target', 'armv6m-none-eabi', '-c', '-O2', '-o', ofile])
+    argv.extend(['-target', 'armv6m-none-eabi', '-c', '-O3', '-o', ofile])
     argv.append('-I'+os.path.expanduser("~/neo/system/include"))
+    argv.append('-I'+os.path.expanduser("~/neo/system/include/MKL46Z4/include/"))
     argv.append('-I'+bench_dir)
-    argv.extend(['-mllvm', '-mserialize=' + bench_pml, '-integrated-as', '-ccc-gcc-name', 'arm-none-eabi-gcc', '--specs=nosys.specs'])
-    
+    argv.extend(['-mllvm', '-mserialize=' + bench_pml, '-mllvm', '-mserialize-all', '-integrated-as', '-ccc-gcc-name', 'arm-none-eabi-gcc', '--specs=nosys.specs'])
+
     # argv.append('-mfloat-abi=softfp') # no improvement
-    
+
     # argv.append('-mfpu=none') # flag does no exist in patmos-clang
-    
+
     argv.append('-fno-builtin')
     # argv.append('-mfpu=vfp')
     argv.append('-mfloat-abi=soft')
     # argv.append('-mhard-float')
 
     argv.append(ll_file)
-    
+
     timed_patmos_clang = eu.TimedCommand(argv, verbose=verbose)
     (stdout, stderr, timeout_occured, returncode) = timed_patmos_clang.run(timeout=timeout)
     if returncode != 0:
@@ -594,14 +597,15 @@ def process_arm_benchmark(benchmark_name, files, out_dir, patmos_clang, patmos_c
     # 4.) build binary from object files
     elf = os.path.join(result_dir, benchmark_name + '.elf')
     argv = [patmos_clang]
-    argv.extend(['-target', 'armv6m-none-eabi', '-integrated-as', '-ccc-gcc-name', 'arm-none-eabi-gcc', '-mthumb', '-DCPU_MKL46Z256VLL4', '-O2', '-o', elf, ofile])
+    argv.extend(['-target', 'armv6m-none-eabi', '-integrated-as', '-ccc-gcc-name', 'arm-none-eabi-gcc', '-mthumb', '-DCPU_MKL46Z256VLL4', '-O3', '-o', elf, ofile])
     argv.extend(helper_objs)
-    argv.extend(['--sysroot', '/opt/gcc-arm-none-eabi-4_9-2014q4//bin', '-I/opt/gcc-arm-none-eabi-4_9-2014q4//arm-none-eabi/include', '-nostdlib', '-Xlinker', '-Map='+str(map_file), '-Xlinker', '--gc-sections', '-T', linker_file])
+    argv.extend(['-g3','-nostdlib', '-Xlinker', '-Map='+str(map_file), '-Xlinker', '--gc-sections', '-T', linker_file])
     argv.append('-I'+bench_dir)
     argv.append('-I'+os.path.expanduser("~/neo/system/include"))
     argv.append('-L'+os.path.expanduser("~/neo/system/include"))
-    argv.append('-lneo')
-   # argv.append('-lneogcc')
+    argv.append('-lneofpu')
+    argv.append('-lneodiv')
+    argv.append('-lneomem')
 
     rep = build_with_fail_report(argv, verbose, timeout, result_file, benchmark_name, result_dir)
     if rep is not None:
@@ -623,20 +627,25 @@ def process_arm_benchmark(benchmark_name, files, out_dir, patmos_clang, patmos_c
     
     # for platin & pasim
     entry = benchmark_name + "_main"
-    
+
     # 4.) platin wcet -i config.pml --enable-wca -b $ELF --disable-ait -e bench_main -i $PML -o wcet.pml --outdir tmp --report report.txt
     platin_wcet_cycles = -1
     platin_trace_cycles = -1
     platin_report = os.path.join(result_dir, 'platin_report.txt')
     wcet_pml = os.path.join(result_dir, 'wcet.pml')
-    
-    argv4 = [platin, 'wcet', '-i', config_pml, '--enable-wca', '-b', elf, '--disable-ait', '-e', entry, '-i', bench_pml, '-o', wcet_pml, '--outdir', result_dir, '--report', platin_report]
+
+    argv4 = [platin, 'wcet', '-i', config_pml, '--enable-wca', '-b', elf,
+            '--disable-ait', '-e', entry, '-i', bench_pml,
+            '-i', os.path.expanduser("~/neo/system/lib/arm-fpu/libneofpu.pml"),
+            '-i', os.path.expanduser("~/neo/system/lib/arm-div/libneodiv.pml"),
+            '-i', os.path.expanduser("~/neo/system/lib/arm-mem/libneomem.pml"),
+            '-o', wcet_pml, '--outdir', result_dir, '--report', platin_report]
     if use_gurobi:
         argv4.append('--wca-use-gurobi')
-    
+
     timed_platin = eu.TimedCommand(argv4, verbose=verbose)
     (stdout, stderr, timeout_occured, returncode) = timed_platin.run(timeout=timeout)
-    
+
     if not timeout_occured:
         ok = True
         # search for WCET in the output of platin