Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux PeSCo 1.7-svn b8d6131600+ SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:44:04 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET
Run set 2ls.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cbmc.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cbmc-path.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] depthk.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] divine-explicit.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] divine-smt.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] esbmc-kind.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] pesco.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] smack.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] symbiotic.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] uautomizer.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] ukojak.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] utaipan.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety]
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -w error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i unreach-call error (134) .084 24 .76 out of memory 200     14000   1800    error (42) 880     1600   12000    timeout 960   6200 7100 unknown 900    1600 13000   unknown 8.0   430   98     unknown 7.9   430   85     true .11  26   .94  unknown 100    2800 1000   disqualified 4.1   120   45    false(unreach-call) 1.3   110 17    timeout 900   1700 11000 timeout 900     5400   11000     timeout 900     1900   12000    
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call error (134) .088 24 .88 out of memory 25     15000   360    error (42) 880     14000   12000    timeout 960   4200 8300 unknown 900    770 11000   unknown 8.2   430   99     unknown 8.1   430   99     timeout 900     2800   11000     timeout 960    4500 7000   disqualified 3.6   91   43    probably out of memory (killed (signal 9, verification)) 290     15000 4000    timeout 900   1600 12000 timeout 900     6200   9600     timeout 900     1300   13000    
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call error (134) .084 24 .74 out of memory 25     15000   270    error (42) 880     14000   12000    timeout 960   4400 6600 unknown 900    770 10000   unknown 8.1   430   93     unknown 8.1   430   120     timeout 900     2800   11000     timeout 960    4700 7200   disqualified 3.6   90   44    probably out of memory (killed (signal 9, verification)) 290     15000 4000    timeout 900   1500 12000 timeout 900     5000   9600     timeout 900     1200   11000    
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call error (134) .078 24 .77 out of memory 72     12000   890    error (42) 870     990   12000    timeout 960   4500 10000 unknown 900    1300 9600   unknown 8.2   430   120     unknown 8.2   430   98     timeout 900     9100   9400     timeout 960    6700 8600   disqualified 880     500   10000    probably out of memory (killed (signal 9, verification)) 350     15000 5200    timeout 900   1300 11000 timeout 900     3800   8600     timeout 900     1400   13000    
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call error (134) .089 24 .66 out of memory 71     12000   800    error (42) 870     2500   12000    timeout 960   4200 9500 unknown 900    1600 9800   unknown 8.2   430   98     unknown 8.3   430   100     timeout 900     8900   9900     timeout 960    8300 9700   disqualified 350     830   3800    probably out of memory (killed (signal 9, verification)) 350     15000 5200    timeout 900   2000 12000 timeout 900     4900   8300     timeout 900     1400   12000    
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call error (134) .080 24 1.0  out of memory 490     10000   4200    out of memory 150     15000   1700    timeout 960   4300 7600 unknown 900    1500 10000   unknown 8.2   430   97     unknown 8.2   430   99     timeout 900     3300   7000     timeout 920    12000 10000   disqualified 17     130   220    false(unreach-call) .17  16 1.8  timeout 900   5400 9200 timeout 900     1200   6500     timeout 900     5300   9400    
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call error (134) .090 24 .89 out of memory 86     15000   1100    error (42) 880     2900   13000    timeout 960   3400 9600 unknown 160    60 2100   timeout 900     1000   11000     timeout 900     2500   9600     timeout 900     11000   9500     timeout 970    5600 8900   disqualified 3.6   91   43    false(unreach-call) 6.6   410 87    timeout 900   830 9000 timeout 900     5100   9000     timeout 900     1000   11000    
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call error (134) .077 24 .86 out of memory 97     15000   1300    error (42) 880     3800   9700    timeout 960   3900 9500 unknown 170    65 2100   timeout 900     740   9200     timeout 900     2500   8000     timeout 900     11000   9100     timeout 960    6000 8000   disqualified 3.7   120   45    false(unreach-call) 8.7   520 120    timeout 900   760 8500 timeout 900     5100   9300     timeout 900     940   9700    
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call error (134) .087 24 .86 out of memory 110     15000   1600    error (42) 880     4900   11000    timeout 960   5000 11000 unknown 210    75 2900   timeout 900     550   7900     timeout 900     2500   9300     timeout 900     11000   8900     timeout 960    5800 8200   disqualified 3.7   95   48    false(unreach-call) 9.7   590 140    timeout 900   910 13000 timeout 900     5200   8600     timeout 900     810   10000    
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call error (134) .090 24 .88 out of memory 120     15000   1600    error (42) 880     5800   11000    timeout 960   3000 11000 unknown 230    82 3100   timeout 900     570   8500     timeout 900     2500   9000     timeout 900     11000   9200     timeout 900    8800 12000   disqualified 3.9   120   51    false(unreach-call) 11     650 150    timeout 900   920 9700 timeout 900     5000   8200     timeout 900     1000   10000    
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call error (134) .083 24 .70 out of memory 94     15000   1400    error (42) 880     6800   12000    timeout 970   4800 10000 unknown 250    84 3400   timeout 900     590   8700     timeout 900     2500   8300     timeout 900     11000   9900     timeout 960    5300 8800   disqualified 3.9   110   49    false(unreach-call) 12     730 170    timeout 900   920 9000 timeout 900     5300   7800     timeout 900     950   11000    
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call error (134) .091 24 .66 out of memory 100     15000   1500    error (42) 880     7800   12000    timeout 970   4700 8700 unknown 280    90 3200   timeout 900     610   8900     timeout 900     2500   8600     timeout 900     11000   10000     timeout 960    5700 8800   disqualified 4.2   100   48    false(unreach-call) 13     820 150    timeout 900   950 12000 timeout 900     4900   8400     timeout 900     1800   12000    
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call error (134) .085 24 .77 out of memory 110     15000   1600    error (42) 880     8700   12000    timeout 960   4500 9800 unknown 280    130 3900   timeout 900     620   8500     timeout 900     2500   8900     timeout 900     11000   9900     timeout 960    6900 8800   disqualified 4.1   130   48    false(unreach-call) 13     910 180    timeout 900   890 11000 timeout 900     5000   8300     timeout 900     980   12000    
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call error (134) .087 24 .74 out of memory 120     15000   1600    error (42) 880     9600   12000    timeout 960   3900 9100 unknown 310    140 4000   timeout 900     640   9800     timeout 900     2500   8400     timeout 900     11000   10000     timeout 960    4500 11000   disqualified 4.3   120   49    false(unreach-call) 15     1000 190    timeout 900   970 13000 timeout 900     5000   8000     timeout 900     1100   10000    
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call error (134) .084 24 .88 out of memory 97     15000   1300    error (42) 880     11000   9700    timeout 960   4400 9500 unknown 330    110 4500   timeout 900     660   9100     timeout 900     2500   8300     timeout 900     10000   11000     timeout 960    5200 8800   disqualified 4.4   120   66    false(unreach-call) 16     1100 210    timeout 900   930 11000 timeout 900     5300   9200     timeout 900     1400   8300    
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call error (134) .081 23 .75 out of memory 64     15000   800    error (42) 880     2900   12000    timeout 960   3300 9300 unknown 120    59 1600   out of memory (unknown error) 170     15000   1600     out of memory (unknown error) 170     15000   1500     timeout 900     6800   11000     timeout 960    3900 7500   disqualified 3.3   85   43    false(unreach-call) 2.1   250 31    timeout 900   1300 10000 timeout 900     5300   7700     timeout 900     940   12000    
array-examples/standard_init1_false-unreach-call_ground.i unreach-call error (134) .081 24 .74 out of memory 100     15000   1600    error (42) 880     1400   15000    timeout 960   3500 11000 unknown 87    51 1100   out of memory (unknown error) 170     15000   1500     out of memory (unknown error) 170     15000   1700     timeout 900     6500   8500     timeout 960    6800 8400   disqualified 3.1   78   39    false(unreach-call) .77  100 11    timeout 900   920 13000 timeout 900     4600   8000     timeout 900     810   11000    
array-examples/standard_init2_false-unreach-call_ground.i unreach-call error (134) .088 24 .70 out of memory 52     15000   800    error (42) 880     2000   15000    timeout 960   2700 9200 unknown 110    59 1400   out of memory (unknown error) 170     15000   1700     out of memory (unknown error) 160     15000   1600     timeout 900     6700   11000     timeout 960    6600 8200   disqualified 3.1   82   38    false(unreach-call) 1.4   190 24    timeout 900   880 9800 timeout 900     5800   8800     timeout 900     770   10000    
array-examples/standard_init3_false-unreach-call_ground.i unreach-call error (134) .080 24 .90 out of memory 57     15000   780    error (42) 880     2600   14000    timeout 970   3700 10000 unknown 120    61 1500   out of memory (unknown error) 170     15000   1700     out of memory (unknown error) 170     15000   1800     timeout 900     6700   9700     timeout 960    5900 8800   disqualified 3.2   84   38    false(unreach-call) 2.0   280 31    timeout 900   860 12000 timeout 900     5200   9300     timeout 900     910   11000    
array-examples/standard_init4_false-unreach-call_ground.i unreach-call error (134) .089 24 .91 out of memory 61     15000   900    error (42) 880     3200   12000    timeout 960   3300 12000 unknown 150    81 2400   out of memory (unknown error) 170     15000   1600     out of memory (unknown error) 170     15000   1700     timeout 900     6600   9400     timeout 960    5200 9400   disqualified 3.2   83   38    false(unreach-call) 2.6   370 38    timeout 900   890 13000 timeout 900     5200   8200     timeout 900     840   11000    
array-examples/standard_init5_false-unreach-call_ground.i unreach-call error (134) .12  24 .58 out of memory 66     15000   920    error (42) 880     3800   11000    timeout 970   4200 9800 unknown 170    76 2100   out of memory (unknown error) 170     15000   1500     out of memory (unknown error) 170     15000   1800     timeout 900     6400   10000     timeout 970    5300 7800   disqualified 3.2   82   39    false(unreach-call) 3.2   460 46    timeout 900   890 10000 timeout 900     5700   8300     timeout 900     750   9600    
array-examples/standard_init6_false-unreach-call_ground.i unreach-call error (134) .086 24 .70 out of memory 70     15000   1000    error (42) 880     4400   12000    timeout 960   2700 7800 unknown 190    98 2400   out of memory (unknown error) 170     15000   1700     out of memory (unknown error) 160     15000   1800     timeout 900     6600   11000     timeout 960    5000 8800   disqualified 3.2   84   42    false(unreach-call) 3.8   540 51    timeout 900   880 9700 timeout 900     6300   11000     timeout 900     720   9100    
array-examples/standard_init7_false-unreach-call_ground.i unreach-call error (134) .083 24 .85 out of memory 75     15000   980    error (42) 880     5000   12000    timeout 960   3200 9200 unknown 210    85 2700   out of memory (unknown error) 170     15000   1700     out of memory (unknown error) 170     15000   1600     timeout 900     6500   10000     timeout 960    5200 7900   disqualified 3.3   87   41    false(unreach-call) 4.5   630 66    timeout 900   810 11000 timeout 900     5300   8700     timeout 900     910   10000    
array-examples/standard_init8_false-unreach-call_ground.i unreach-call error (134) .11  24 .69 out of memory 54     15000   720    error (42) 880     5600   11000    timeout 970   4400 9300 unknown 240    110 3400   out of memory (unknown error) 170     15000   1600     out of memory (unknown error) 170     15000   1800     timeout 900     6700   8800     timeout 970    5100 8600   disqualified 3.3   85   45    false(unreach-call) 5.1   720 70    timeout 900   880 9000 timeout 900     5400   7500     timeout 900     770   9600    
array-examples/standard_init9_false-unreach-call_ground.i unreach-call error (134) .085 24 .86 out of memory 57     15000   900    error (42) 880     6200   14000    timeout 960   3700 10000 unknown 260    98 3400   out of memory (unknown error) 160     15000   1700     out of memory (unknown error) 170     15000   1800     timeout 900     6700   10000     timeout 970    7000 7800   disqualified 3.4   110   37    false(unreach-call) 5.6   810 90    timeout 900   900 9300 timeout 900     5000   8100     timeout 900     930   11000    
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call error (134) .088 24 .72 error (42) 880     1100   4000    error (42) 870     960   12000    timeout 960   4300 9300 unknown 110    64 1300   unknown 8.2   430   95     unknown 8.1   430   130     timeout 900     8500   10000     timeout 960    4800 9000   disqualified 3.2   83   37    false(unreach-call) .99  100 12    timeout 900   1700 11000 timeout 900     5500   11000     timeout 900     1200   12000    
array-examples/standard_partition_false-unreach-call_ground.i unreach-call error (134) .082 24 .76 out of memory 170     14000   2000    error (42) 880     3300   14000    timeout 960   4300 10000 unknown 300    120 3700   unknown 8.6   430   120     timeout 900     1400   7600     timeout 900     4400   11000     timeout 960    4300 7600   disqualified 4.1   93   50    timeout (verification) 900     2800 7700    timeout 900   1300 11000 timeout 900     5200   8800     timeout 900     900   8100    
array-examples/standard_running_false-unreach-call.i unreach-call error (134) .12  23 .65 out of memory 82     15000   1200    out of memory 300     15000   4500    timeout 970   4600 8500 unknown 260    130 3500   unknown 8.2   430   100     unknown 8.3   430   94     out of memory 390     15000   5300     timeout 960    4800 10000   disqualified 3.0   85   37    false(unreach-call) 1.9   180 29    timeout 900   1300 13000 timeout 900     6700   8800     timeout 900     1100   12000    
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call error (134) .094 24 .67 true 130     4200   1600    true 130     2900   1700    true 93   1300 1100 unknown 900    2700 9000   true 21     430   220     true 21     430   240     true .10  26   1.1   true 11    1200 80   disqualified 3.4   100   51    true .97  95 15    true 9.4 370 83 timeout 900     2100   9800     true 8.7   350   81    
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call error (134) .087 24 .70 error (42) 880     9800   12000    error (42) 880     1300   14000    timeout 970   5500 11000 unknown 900    1200 12000   unknown 8.1   430   99     unknown 8.1   430   110     true .14  26   .99  unknown 100    2000 1300   disqualified 880     210   14000    true 1.1   86 16    timeout 900   5500 10000 timeout 900     5300   9400     timeout 900     2000   12000    
array-examples/relax_true-unreach-call.i unreach-call error (134) .18  26 1.3  out of memory 280     13000   3400    out of memory 200     15000   2500    timeout 970   6800 8400 unknown 900    170 13000   unknown 8.5   450   120     unknown 1.6   200   21     timeout 900     340   13000     timeout 960    5100 10000   disqualified 880     340   9800    timeout (verification) 900     750 11000    timeout 900   730 11000 timeout 900     690   13000     timeout 900     930   12000    
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call error (134) .088 23 .68 error (42) 880     2100   4300    error (42) 880     1300   13000    timeout 960   4400 10000 unknown 200    100 2400   unknown 48     430   610     unknown 48     430   690     timeout 900     12000   9700     timeout 960    4100 9000   disqualified 2.7   80   30    true 1.7   95 24    timeout 900   1700 14000 timeout 900     5700   8000     timeout 900     1300   12000    
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call error (134) .093 24 .68 error (42) 880     13000   11000    error (42) 880     13000   11000    timeout 910   1000 10000 unknown 320    83 4500   unknown 8.2   430   110     unknown 8.4   430   120     true .13  26   1.2   out of memory 840    15000 11000   disqualified 5.7   94   73    true 1.4   68 21    timeout 900   1800 11000 timeout 900     1600   8800     timeout 900     1200   12000    
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call error (134) .089 24 .69 error (42) 880     2700   10000    error (42) 880     1800   12000    true 14   630 110 unknown .79 67 9.3 unknown 8.3   430   120     unknown 8.6   430   130     true .088 26   1.1   true 18    1400 130   disqualified 880     350   11000    timeout (verification) 900     1200 10000    true 9.5 380 75 true 9.3   370   74     true 8.9   360   67    
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call error (134) .081 24 .99 error (42) 880     1100   4300    error (42) 880     980   12000    timeout 960   4200 12000 unknown 93    69 1200   unknown 8.1   430   110     unknown 8.3   430   110     timeout 900     8600   10000     timeout 960    5200 9100   disqualified 3.0   83   41    true 1.1   62 14    timeout 900   1600 14000 timeout 900     4900   9400     timeout 900     1200   11000    
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call error (134) .083 24 .69 out of memory 95     15000   1600    out of memory 84     15000   1100    true 93   1100 1100 unknown .80 66 9.3 out of memory (unknown error) 170     15000   1800     out of memory (unknown error) 170     15000   1800     true .089 26   .86  true 13    1000 93   disqualified 2.0   73   25    true .14  16 1.4  true 7.9 360 59 true 7.5   370   69     true 7.7   370   59    
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call error (134) .084 24 .74 out of memory 24     15000   320    error (42) 880     15000   13000    timeout 960   4200 7000 unknown 900    780 9800   unknown 8.4   430   97     unknown 8.1   430   110     timeout 900     2800   10000     timeout 960    4500 7700   disqualified 22     140   310    probably out of memory (killed (signal 9, verification)) 290     15000 3700    timeout 900   1700 9800 timeout 900     5200   8500     timeout 900     1700   11000    
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call error (134) .088 24 .81 out of memory 72     12000   820    error (42) 870     2500   12000    timeout 960   4200 9400 unknown 900    1600 8600   unknown 8.1   430   93     unknown 8.2   430   110     timeout 900     9100   10000     timeout 960    6800 9700   disqualified 880     780   9600    probably out of memory (killed (signal 9, verification)) 350     15000 4900    timeout 900   1300 13000 timeout 900     3500   8800     timeout 900     1300   12000    
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call error (134) .079 23 .68 out of memory 120     15000   1500    error (42) 880     1700   12000    timeout 970   4100 7800 unknown 150    72 1800   unknown 8.2   430   100     unknown 8.2   430   110     timeout 900     6700   9800     timeout 900    7300 12000   disqualified 2.5   81   34    true 2.1   100 23    timeout 900   710 10000 timeout 900     5800   10000     timeout 900     850   12000    
array-examples/standard_compare_true-unreach-call_ground.i unreach-call error (134) .080 23 .90 error (42) 880     1100   4600    error (42) 880     1300   11000    timeout 970   4500 9700 unknown 65    56 880   unknown 8.0   430   99     unknown 8.1   430   96     timeout 900     9300   9000     timeout 900    1800 11000   disqualified 2.7   84   36    true 1.3   63 17    timeout 900   880 11000 timeout 900     5000   10000     timeout 900     940   11000    
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call error (134) .080 24 .97 out of memory 59     15000   880    error (42) 880     2300   12000    timeout 960   4700 13000 unknown 160    59 2100   unknown 890     1500   11000     timeout 900     2300   8500     timeout 900     11000   9700     timeout 960    4900 11000   disqualified 3.2   82   38    true 2.9   230 38    timeout 900   930 10000 timeout 900     5200   8200     timeout 900     1000   9800    
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call error (134) .089 24 .73 out of memory 71     15000   990    error (42) 880     3200   14000    timeout 970   4600 9500 unknown 170    66 2400   timeout 900     1000   9200     timeout 900     2300   8500     timeout 900     11000   9700     timeout 960    5300 8800   disqualified 3.3   85   39    true 3.3   250 41    timeout 900   850 9800 timeout 900     5300   8900     timeout 900     820   11000    
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call error (134) .077 24 .92 out of memory 82     15000   1200    error (42) 870     4200   13000    timeout 960   4200 10000 unknown 190    84 2500   timeout 900     770   9400     timeout 900     2300   8400     timeout 900     11000   11000     timeout 970    5800 8100   disqualified 3.5   89   47    true 3.9   280 45    timeout 900   740 11000 timeout 900     5200   8100     timeout 900     820   10000    
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call error (134) .082 24 .70 out of memory 95     15000   1300    error (42) 880     5300   12000    timeout 960   4100 10000 unknown 210    84 3100   timeout 900     610   9800     timeout 900     2300   7800     timeout 900     12000   12000     timeout 900    7800 14000   disqualified 3.7   93   47    true 4.3   300 55    timeout 900   750 8500 timeout 900     4700   8000     timeout 900     840   10000    
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call error (134) .099 24 .65 out of memory 110     15000   1400    error (42) 880     6200   12000    timeout 970   4900 8800 unknown 260    98 3300   timeout 900     630   9000     timeout 900     2300   9100     timeout 900     11000   11000     timeout 960    6000 9900   disqualified 3.8   95   54    true 4.9   330 67    timeout 900   760 10000 timeout 900     5300   10000     timeout 900     990   11000    
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call error (134) .079 24 .77 out of memory 87     15000   1200    error (42) 880     7200   12000    timeout 960   3800 11000 unknown 280    99 3500   timeout 900     650   8200     timeout 900     2300   9200     timeout 900     12000   11000     timeout 970    7300 9200   disqualified 4.0   100   50    true 5.3   350 75    timeout 900   920 9900 timeout 900     5200   8600     timeout 900     990   9100    
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call error (134) .098 23 .73 out of memory 96     15000   1200    error (42) 880     8100   14000    timeout 960   4700 9200 unknown 300    100 4100   timeout 900     670   9000     timeout 900     2300   8700     timeout 900     12000   10000     timeout 960    6000 9400   disqualified 4.2   100   53    true 5.8   380 79    timeout 900   890 9900 timeout 900     5200   7900     timeout 900     1100   11000    
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call error (134) .088 24 .76 out of memory 110     15000   1700    error (42) 880     9100   12000    timeout 960   4300 9100 unknown 350    110 4600   timeout 900     700   10000     timeout 900     2300   8100     timeout 900     12000   9400     timeout 960    7200 9200   disqualified 4.4   100   58    true 6.4   400 94    timeout 900   940 10000 timeout 900     5300   8500     timeout 900     1000   8000    
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call error (134) .084 24 .99 out of memory 110     15000   1600    error (42) 880     10000   11000    timeout 970   4300 9500 unknown 360    120 5300   timeout 900     720   9900     timeout 900     2200   7900     timeout 900     11000   10000     timeout 960    6200 10000   disqualified 4.6   110   58    true 7.0   430 95    timeout 900   790 9200 timeout 900     4400   8900     timeout 900     1100   9000    
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call error (134) .098 24 .84 out of memory 64     15000   940    error (42) 880     2900   14000    timeout 960   2700 7000 unknown 130    73 1700   out of memory (unknown error) 170     15000   1600     out of memory (unknown error) 160     15000   1500     timeout 900     6800   11000     timeout 970    5900 8500   disqualified 3.2   87   39    true 1.8   99 26    timeout 900   910 8800 timeout 900     5300   11000     timeout 900     730   9200    
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call error (134) .11  24 .62 out of memory 68     15000   920    error (42) 880     3500   12000    timeout 960   3400 9700 unknown 170    91 2300   out of memory (unknown error) 160     15000   1600     out of memory (unknown error) 170     15000   1600     timeout 900     6800   10000     timeout 960    4400 8600   disqualified 3.9   92   50    true 2.2   120 31    timeout 900   960 13000 timeout 900     6100   9400     timeout 900     930   9000    
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call error (134) .088 24 .73 out of memory 64     15000   820    error (42) 880     2900   10000    timeout 960   3900 9900 unknown 130    70 1700   out of memory (unknown error) 170     15000   1600     out of memory (unknown error) 170     15000   1500     timeout 900     6700   8500     timeout 970    3800 8400   disqualified 3.0   83   35    true 1.8   140 26    timeout 900   920 11000 timeout 900     5100   9400     timeout 900     780   11000    
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call error (134) .082 24 .76 out of memory 59     15000   870    error (42) 880     2300   11000    timeout 960   2600 8900 unknown 100    54 1400   out of memory (unknown error) 170     15000   1700     out of memory (unknown error) 170     15000   1500     timeout 900     6500   9600     timeout 970    7700 7700   disqualified 2.8   84   33    true 1.3   81 20    timeout 900   740 9900 timeout 900     5100   7500     timeout 900     760   9800    
array-examples/standard_find_true-unreach-call_ground.i unreach-call error (134) .087 24 .69 out of memory 100     15000   1400    error (42) 880     1400   12000    timeout 970   4600 11000 unknown 230    110 3800   unknown 360     950   4000     timeout 900     2300   8000     timeout 900     11000   11000     timeout 900    7400 13000   disqualified 3.5   89   41    error(unknown, verification-finished) 350     2400 4800    timeout 900   930 9500 timeout 900     5000   9700     timeout 900     1300   13000    
array-examples/standard_init1_true-unreach-call_ground.i unreach-call error (134) .090 24 .71 out of memory 100     15000   1400    error (42) 870     1400   11000    timeout 960   2800 8300 unknown 87    51 1100   out of memory (unknown error) 170     15000   1600     out of memory (unknown error) 170     15000   1600     timeout 900     6600   11000     timeout 960    6700 8400   disqualified 2.6   79   37    true .92  63 14    timeout 900   910 10000 timeout 900     5200   6700     timeout 900     930   11000    
array-examples/standard_init2_true-unreach-call_ground.i unreach-call error (134) .086 24 .91 out of memory 52     15000   630    error (42) 870     2000   12000    timeout 960   2800 8900 unknown 110    60 1700   out of memory (unknown error) 170     15000   1900     out of memory (unknown error) 160     15000   1600     timeout 900     6600   13000     timeout 970    7700 8400   disqualified 2.7   77   29    true 1.2   79 17    timeout 900   730 9600 timeout 900     5200   8100     timeout 900     960   13000    
array-examples/standard_init3_true-unreach-call_ground.i unreach-call error (134) .081 24 .67 out of memory 57     15000   920    error (42) 880     2600   13000    timeout 960   3300 8600 unknown 120    60 1400   out of memory (unknown error) 170     15000   1600     out of memory (unknown error) 170     15000   1500     timeout 900     6400   9500     timeout 960    7500 8200   disqualified 2.7   80   40    true 1.5   96 20    timeout 900   760 13000 timeout 900     5200   10000     timeout 900     710   12000    
array-examples/standard_init4_true-unreach-call_ground.i unreach-call error (134) .085 24 .70 out of memory 61     15000   850    error (42) 880     3200   14000    timeout 970   4500 10000 unknown 150    81 2100   out of memory (unknown error) 170     15000   1700     out of memory (unknown error) 170     15000   1500     timeout 900     6500   12000     timeout 960    5500 8500   disqualified 2.9   84   36    true 1.8   110 25    timeout 900   880 9700 timeout 900     4500   8200     timeout 900     700   11000    
array-examples/standard_init5_true-unreach-call_ground.i unreach-call error (134) .11  24 .61 out of memory 66     15000   960    error (42) 880     3800   11000    timeout 970   4200 11000 unknown 170    77 2300   out of memory (unknown error) 170     15000   1700     out of memory (unknown error) 160     15000   1600     timeout 900     6600   10000     timeout 960    4900 8000   disqualified 2.9   85   39    true 2.0   130 28    timeout 900   730 9100 timeout 900     6200   8400     timeout 900     870   11000    
array-examples/standard_init6_true-unreach-call_ground.i unreach-call error (134) .085 23 1.2  out of memory 70     15000   950    error (42) 880     4400   12000    timeout 960   3100 9200 unknown 190    98 2900   out of memory (unknown error) 170     15000   1700     out of memory (unknown error) 160     15000   1500     timeout 900     6400   10000     timeout 960    5200 7800   disqualified 3.0   88   37    true 2.3   140 33    timeout 900   840 9000 timeout 900     5100   7700     timeout 900     870   8800    
array-examples/standard_init7_true-unreach-call_ground.i unreach-call error (134) .082 24 .68 out of memory 75     15000   1100    error (42) 880     5000   11000    timeout 970   4400 10000 unknown 210    85 2500   out of memory (unknown error) 160     15000   1700     out of memory (unknown error) 160     15000   1600     timeout 900     6500   11000     timeout 970    7300 9400   disqualified 3.0   86   42    true 2.5   160 38    timeout 900   820 8500 timeout 900     5000   8000     timeout 900     870   9100    
array-examples/standard_init8_true-unreach-call_ground.i unreach-call error (134) .13  24 .72 out of memory 54     15000   790    error (42) 880     5600   13000    timeout 960   2700 7800 unknown 240    110 3100   out of memory (unknown error) 170     15000   1600     out of memory (unknown error) 160     15000   1700     timeout 900     6600   11000     timeout 970    6900 9200   disqualified 3.1   91   38    true 2.8   180 39    timeout 900   880 8300 timeout 900     5300   8500     timeout 900     770   8100    
array-examples/standard_init9_true-unreach-call_ground.i unreach-call error (134) .084 24 .82 out of memory 57     15000   860    error (42) 880     6200   11000    timeout 960   3400 9400 unknown 260    98 3100   out of memory (unknown error) 170     15000   1600     out of memory (unknown error) 170     15000   1600     timeout 900     6500   9400     timeout 960    7100 8400   disqualified 3.2   91   38    true 3.0   190 45    timeout 900   770 8700 timeout 900     3700   9400     timeout 900     920   10000    
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call error (134) .090 24 .62 error (42) 880     1100   4800    error (42) 880     980   14000    timeout 970   5000 7600 unknown 93    70 1200   unknown 8.4   430   97     unknown 8.0   430   120     timeout 900     8600   10000     timeout 960    4700 7200   disqualified 3.0   83   36    true 1.0   64 13    timeout 900   1800 13000 timeout 900     6400   8600     timeout 900     1300   12000    
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call error (134) .078 23 .89 error (42) 880     1100   4700    error (42) 880     980   12000    timeout 960   4500 8000 unknown 120    66 1400   unknown 8.3   430   95     unknown 8.2   430   97     timeout 900     8700   10000     timeout 970    6100 9900   disqualified 3.0   83   37    true 1.1   64 14    timeout 900   1700 11000 timeout 900     6100   8100     timeout 900     1200   12000    
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call error (134) .080 24 .85 out of memory 150     13000   1900    error (42) 880     3700   12000    timeout 960   4200 9200 unknown 140    57 2200   unknown 180     680   2300     unknown 180     680   2000     timeout 900     12000   10000     timeout 970    7400 10000   disqualified 2.5   77   28    true .68  39 9.0  timeout 900   890 11000 timeout 900     4800   8300     timeout 900     910   10000    
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call error (134) .082 24 .91 error (42) 880     7000   13000    error (42) 880     1700   14000    timeout 970   4500 12000 unknown 300    110 3800   unknown 8.1   430   96     unknown 8.2   430   100     timeout 900     4200   11000     timeout 960    4800 7600   disqualified 140     110   1900    true 2.0   120 29    timeout 900   940 11000 timeout 900     5300   7300     timeout 900     1000   10000    
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call error (134) .081 24 .86 out of memory 140     14000   1700    error (42) 870     2000   13000    timeout 970   4100 11000 unknown 300    86 4500   unknown 8.3   430   110     unknown 8.2   430   120     out of memory 430     15000   5600     timeout 960    5400 9100   disqualified 68     100   910    true 1.3   84 21    timeout 900   930 11000 timeout 900     5300   8600     timeout 900     1000   11000    
array-examples/standard_partition_true-unreach-call_ground.i unreach-call error (134) .089 24 .81 out of memory 160     14000   1900    error (42) 880     3000   12000    timeout 960   4400 12000 unknown 150    71 1800   unknown 8.1   430   93     unknown 8.2   430   90     timeout 900     4200   12000     timeout 960    4000 9200   disqualified 24     93   340    true .58  47 9.0  timeout 900   1300 11000 timeout 900     5400   7900     timeout 900     1000   12000    
array-examples/standard_password_true-unreach-call_ground.i unreach-call error (134) .091 24 .71 error (42) 880     1100   4000    error (42) 880     1300   13000    timeout 960   4600 9600 unknown 65    56 760   unknown 8.2   430   100     unknown 8.1   430   96     timeout 900     9100   10000     timeout 900    2300 12000   disqualified 2.7   85   32    true 1.3   63 18    timeout 900   910 12000 timeout 900     4900   8400     timeout 900     930   10000    
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call error (134) .077 23 .80 out of memory 150     13000   2000    error (42) 880     4100   12000    timeout 970   4800 8000 unknown 140    84 1800   unknown 450     950   5500     unknown 450     950   5500     timeout 900     10000   12000     unknown 100    1500 1300   disqualified 2.7   82   36    true 1.2   64 17    timeout 900   920 12000 timeout 900     4600   7900     timeout 900     1000   12000    
array-examples/standard_running_true-unreach-call.i unreach-call error (134) .088 23 .68 out of memory 82     15000   1200    out of memory 310     15000   4100    timeout 960   4600 8100 unknown 900    1700 10000   unknown 8.1   430   120     unknown 8.1   430   100     out of memory 390     15000   4600     timeout 970    3900 8200   disqualified 2.7   80   34    true 1.1   45 16    timeout 900   1600 13000 timeout 900     5300   8700     timeout 900     1400   13000    
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call error (134) .12  24 .65 error (42) 880     2500   12000    error (42) 880     2600   11000    timeout 960   4100 11000 unknown 55    44 810   unknown 48     430   660     true 8.8   370   110     timeout 900     330   12000     true 15    1200 98   disqualified 2.7   75   28    timeout (verification) 900     2600 4100    true 13   500 110 true 15     640   120     true 14     570   130    
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call error (134) .081 23 .78 out of memory 150     13000   2200    error (42) 880     3800   12000    timeout 960   2500 8500 unknown 120    56 1600   out of memory (unknown error) 170     15000   1700     out of memory (unknown error) 170     15000   1700     timeout 900     7600   13000     timeout 900    7600 11000   disqualified 2.8   82   36    true 1.1   64 18    timeout 900   670 13000 timeout 900     5100   7800     timeout 900     980   13000    
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call error (134) .080 23 .80 error (42) 880     2600   6400    error (42) 880     1200   12000    timeout 960   4400 8600 unknown 56    55 800   unknown 89     430   1400     unknown 88     430   1200     timeout 900     8400   10000     timeout 970    7000 8400   disqualified 2.7   82   37    true 1.3   79 22    timeout 900   1100 11000 timeout 900     5600   8500     timeout 900     4300   5400    
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call error (134) .084 24 .69 out of memory 64     15000   800    error (42) 880     2100   14000    timeout 970   4300 8600 unknown 120    63 1600   unknown 450     950   5300     timeout 900     2200   8500     timeout 900     12000   9700     timeout 960    6900 7500   disqualified 7.6   100   100    error(unknown, verification-finished) 170     2300 2300    timeout 900   760 11000 timeout 900     3700   11000     timeout 900     910   12000    
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call error (134) .085 24 .75 out of memory 64     15000   950    error (42) 880     2200   12000    timeout 960   4100 9500 unknown 190    140 2600   unknown 450     950   4900     timeout 900     2300   8100     timeout 900     12000   11000     timeout 970    6400 9200   disqualified 5.7   98   76    error(unknown, verification-finished) 160     2400 1900    timeout 900   900 11000 timeout 900     4000   11000     timeout 900     1000   11000    
array-examples/standard_two_index_01_true-unreach-call.i unreach-call out of memory 300     15000 2000    out of memory 71     15000   930    error (42) 870     840   13000    timeout 970   9200 6100 unknown 120    59 1800   unknown 23     520   270     timeout 900     1300   7900     timeout 900     12000   11000     timeout 960    9900 10000   disqualified 880     870   9100    true .40  34 5.2  timeout 900   910 9600 timeout 900     5300   8200     timeout 900     940   12000    
array-examples/standard_two_index_02_true-unreach-call.i unreach-call error (134) .084 24 .67 out of memory 160     13000   2100    error (42) 880     4300   13000    timeout 970   4100 12000 unknown 180    66 2800   unknown 670     1200   8000     timeout 900     2300   7800     timeout 900     11000   11000     timeout 960    5800 9100   disqualified 2.7   81   34    true 2.4   190 29    timeout 900   860 10000 timeout 900     4300   7900     timeout 900     990   10000    
array-examples/standard_two_index_03_true-unreach-call.i unreach-call out of memory 250     15000 2200    out of memory 97     13000   1500    error (42) 880     960   12000    timeout 960   9900 8900 unknown 140    63 2200   unknown 18     490   200     timeout 900     1300   7800     timeout 900     12000   9100     timeout 960    7600 8200   disqualified 900     4400   13000    true .33  31 4.9  timeout 900   730 11000 timeout 900     5300   7900     timeout 900     890   11000    
array-examples/standard_two_index_04_true-unreach-call.i unreach-call error (134) .087 24 .66 out of memory 150     13000   2600    error (42) 880     4600   12000    timeout 970   4600 8700 unknown 160    64 2500   unknown 560     1100   6400     timeout 900     2300   8600     timeout 900     11000   9900     timeout 960    6500 9800   disqualified 2.6   82   37    true 2.1   180 24    timeout 900   740 12000 timeout 900     5100   9600     timeout 900     1100   10000    
array-examples/standard_two_index_05_true-unreach-call.i unreach-call error (134) .081 24 .80 out of memory 160     13000   2100    error (42) 880     4700   12000    timeout 960   2800 9500 unknown 150    68 2200   unknown 540     1100   6300     timeout 900     2300   8400     timeout 900     12000   12000     timeout 960    7700 9400   disqualified 2.5   81   37    true 1.9   180 27    timeout 900   750 8600 timeout 900     3800   7700     timeout 900     1100   11000    
array-examples/standard_two_index_06_true-unreach-call.i unreach-call out of memory 230     15000 1600    out of memory 97     13000   1500    error (42) 880     970   13000    timeout 960   9700 10000 unknown 160    65 1900   unknown 17     480   210     timeout 900     1300   8300     timeout 900     12000   9800     timeout 970    8000 9200   disqualified 890     1100   11000    true .32  29 3.5  timeout 900   730 12000 timeout 900     5200   10000     timeout 900     980   11000    
array-examples/standard_two_index_07_true-unreach-call.i unreach-call error (134) .082 23 .84 out of memory 160     13000   2000    error (42) 880     4300   12000    timeout 970   3900 7200 unknown 160    71 1900   unknown 510     1000   5600     timeout 900     2300   9200     timeout 900     12000   9900     timeout 960    5400 8400   disqualified 2.5   81   39    true 1.9   180 24    timeout 900   910 9000 timeout 900     5100   7600     timeout 900     1100   13000    
array-examples/standard_two_index_08_true-unreach-call.i unreach-call error (134) .087 24 1.0  out of memory 160     13000   2100    error (42) 880     4300   11000    timeout 970   4000 10000 unknown 160    67 2000   unknown 500     1000   6200     timeout 900     2300   8200     timeout 900     12000   10000     timeout 960    4900 8500   disqualified 2.5   81   32    true 1.9   180 25    timeout 900   930 9800 timeout 900     5200   8400     timeout 900     1100   12000    
array-examples/standard_two_index_09_true-unreach-call.i unreach-call error (134) .11  24 .73 out of memory 160     13000   2500    error (42) 880     4700   11000    timeout 970   3600 9000 unknown 170    70 2200   unknown 500     1000   5500     timeout 900     2300   8100     timeout 900     12000   9800     timeout 970    7900 8700   disqualified 2.4   74   29    true 1.9   180 23    timeout 900   920 9700 timeout 900     5200   8000     timeout 900     1100   12000    
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call error (134) .081 24 .77 error (42) 880     1800   8800    error (42) 880     790   11000    timeout 960   6100 7400 unknown 60    51 920   unknown 8.2   430   93     unknown 8.1   430   100     timeout 900     1000   11000     timeout 940    5900 7100   disqualified 880     380   11000    true .14  15 1.5  timeout 900   1200 11000 timeout 900     970   7300     timeout 900     960   13000    
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call error (134) .086 24 .69 out of memory 120     15000   1700    error (42) 880     2000   11000    timeout 960   4100 11000 unknown 130    73 1700   unknown 540     950   6200     unknown 540     950   7300     timeout 900     5400   13000     timeout 960    6100 7700   disqualified 2.9   86   39    true 1.5   67 20    timeout 900   680 12000 timeout 900     3400   7900     timeout 900     750   11000    
array-examples/standard_sentinel_true-unreach-call.i.v+cfa-reducer.c unreach-call error (134) .094 24 .74 error (42) 880     2500   13000    error (42) 880     2700   11000    timeout 960   4300 10000 unknown 55    44 700   unknown 48     430   670     true 9.2   370   130     timeout 900     330   12000     timeout 960    5100 12000   disqualified 2.7   75   33    timeout (verification) 900     2600 4200    true 15   650 140 true 17     650   130     true 15     660   120    
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call error (134) .10  24 .84 out of memory 52     15000   630    error (42) 870     1800   12000    timeout 970   4000 9700 unknown 1.2  67 13   out of memory (unknown error) 170     15000   1600     out of memory (unknown error) 160     15000   1500     timeout 900     7400   9900     timeout 960    5400 8900   disqualified 3.1   82   38    false(unreach-call) .79  110 12    timeout 900   1000 10000 timeout 900     5000   8600     timeout 900     1100   9400    
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call out of memory 35     15000 510    out of memory 290     15000   3100    out of memory 23     8000   230    timeout 960   3700 7700 unknown 1.2  67 15   out of memory (unknown error) 170     15000   1800     out of memory (unknown error) 170     15000   1600     timeout 900     6400   10000     timeout 960    6900 7100   disqualified 3.2   82   38    false(unreach-call) .78  110 9.8  timeout 900   1500 10000 timeout 900     5100   7800     timeout 900     4900   9200    
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call error (134) .086 24 .83 out of memory 68     15000   980    out of memory 190     15000   3100    timeout 970   4700 12000 unknown 230    66 3100   unknown 8.2   430   97     timeout 900     12000   7000     timeout 900     4900   11000     timeout 900    6500 12000   disqualified 4.4   110   53    false(unreach-call) 1.7   200 22    timeout 900   1100 9300 timeout 900     5100   9500     timeout 900     1200   10000    
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call true 42     15000 480    out of memory 380     15000   4900    out of memory 280     15000   3700    timeout 960   3800 10000 unknown 210    55 2900   false(unreach-call) 400     3700   4300     false(unreach-call) 400     3700   4600     timeout 900     5200   10000     timeout 960    6200 7900   disqualified 3.1   85   38    false(unreach-call) 1.0   120 14    timeout 900   1200 8800 timeout 900     5300   7100     timeout 900     4100   9100    
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call error (134) .090 24 .82 out of memory 68     15000   880    out of memory 190     15000   2900    timeout 970   4000 9500 unknown 180    81 2500   unknown 8.2   430   98     timeout 900     13000   7100     timeout 900     4900   10000     timeout 900    6800 11000   disqualified 4.5   120   58    timeout (verification) 900     2600 10000    timeout 900   1100 11000 timeout 900     5000   7500     timeout 900     1200   8900    
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call error (134) .087 24 .76 out of memory 66     14000   880    error (42) 880     1800   13000    timeout 970   5700 9100 unknown 900    1300 11000   unknown 8.1   430   120     unknown 8.2   430   91     timeout 900     3400   10000     timeout 910    7900 12000   disqualified 5.9   110   76    false(unreach-call) 1.7   320 23    timeout 900   1700 14000 timeout 900     5300   9600     timeout 900     1500   13000    
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call error (134) .081 24 .76 out of memory 89     15000   1400    error (42) 880     1900   12000    timeout 970   4800 9800 unknown 170    58 2200   unknown 8.3   430   95     timeout 900     4200   5200     timeout 900     4000   9700     timeout 960    4800 9100   disqualified 2.7   84   40    timeout (verification) 900     2600 13000    timeout 900   770 11000 timeout 900     5300   7500     timeout 900     910   11000    
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call error (134) .080 24 .80 out of memory 100     15000   1400    error (42) 880     2700   14000    timeout 970   4200 8400 unknown 900    340 11000   out of memory (unknown error) 270     15000   2700     out of memory (unknown error) 270     15000   3100     timeout 900     4400   10000     timeout 910    7900 11000   disqualified 880     260   12000    timeout (verification) 900     3100 9600    timeout 900   890 10000 timeout 900     3800   8300     timeout 900     820   12000    
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call true 36     13000 480    out of memory 210     15000   2600    out of memory 760     15000   9100    timeout 970   6800 7300 unknown 740    1400 8000   unknown 8.2   430   91     timeout 900     6200   9100     out of memory 570     15000   4600     timeout 960    6900 8100   disqualified 2.7   84   30    true .95  69 14    timeout 900   1400 12000 timeout 900     5200   11000     timeout 900     4900   9800    
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call error (134) 240     7000 1800    out of memory 310     15000   4200    error (134) 2.6   400   30    timeout 970   4800 8400 unknown .81 65 8.7 unknown 8.3   440   99     timeout 900     4700   8600     timeout 900     5300   10000     timeout 910    5300 6800   disqualified 8.6   100   120    timeout (verification) 900     3200 14000    timeout 900   1200 9300 timeout 900     5200   6600     timeout 900     4000   6200    
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call error (134) .18  24 1.2  out of memory 180     15000   2100    error (42) 880     2000   12000    timeout 960   4800 7200 unknown 400    590 4500   out of memory (unknown error) 120     15000   1300     out of memory (unknown error) 120     15000   1200     timeout 900     13000   10000     timeout 970    7600 8600   disqualified 3.0   83   35    true 1.2   100 17    true 15   500 120 timeout 900     5300   7600     true 18     650   140    
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call error (134) 160     7000 1100    out of memory 310     15000   4000    error (134) 2.5   400   29    timeout 960   4000 8800 unknown .83 67 8.4 unknown 8.3   440   110     timeout 900     4600   9100     timeout 900     4900   10000     timeout 930    5700 6900   disqualified 2.9   80   37    timeout (verification) 900     4000 12000    timeout 900   1000 8700 timeout 900     5400   8800     timeout 900     4000   6200    
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call out of memory 36     15000 440    out of memory 410     15000   5000    error (134) 5.3   500   51    timeout 960   4000 8900 unknown 900    1500 9200   out of memory (unknown error) 170     15000   1900     out of memory (unknown error) 170     15000   1800     timeout 900     3000   14000     timeout 960    6300 10000   disqualified 880     440   9300    timeout (verification) 900     2800 9400    timeout 900   1700 11000 timeout 900     2700   8800     timeout 900     5200   8100    
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call out of memory 28     15000 450    out of memory 89     15000   1200    out of memory 22     9200   320    timeout 960   3900 10000 unknown 900    2200 12000   unknown 8.3   440   97     unknown 8.5   440   110     timeout 900     1700   13000     timeout 900    6900 13000   disqualified 5.9   97   84    true 1.4   110 16    timeout 900   1300 8100 timeout 900     5400   10000     timeout 900     5000   6500    
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call timeout 900     11000 7900    error (42) 870     13000   12000    error (42) 880     10000   10000    timeout 960   3700 7900 unknown 900    1900 9600   out of memory (unknown error) 130     15000   1300     out of memory (unknown error) 130     15000   1200     timeout 900     9100   11000     timeout 900    5600 8600   disqualified 2.7   84   34    true 1.1   82 16    timeout 900   1200 9700 timeout 900     5200   7400     timeout 900     4700   6800    
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call error (134) 260     6900 1900    out of memory 320     15000   4100    error (134) 6.7   400   69    timeout 970   4900 7300 unknown 900    2200 8700   unknown 8.3   440   120     timeout 900     9400   8100     timeout 900     4300   9000     timeout 960    5700 7000   disqualified 19     120   250    timeout (verification) 900     4200 12000    timeout 900   1300 9800 timeout 900     5400   8800     timeout 900     4400   6500    
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call timeout 900     12000 4500    out of memory 510     13000   6400    error (42) 870     4500   10000    timeout 960   5500 7700 unknown 900    83 11000   unknown 8.3   430   120     unknown 1.5   200   25     timeout 900     150   11000     timeout 960    6000 9500   disqualified 880     380   12000    timeout (verification) 900     1100 10000    timeout 900   1000 8600 timeout 900     1000   7800     timeout 900     920   7300    
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call error (134) .087 24 .71 false(unreach-call) .13  9.3 .89 false(unreach-call) .16  8.9 1.2  exception 380   2300 2800 false(unreach-call) 6.0  69 61   unknown 8.2   430   100     false(unreach-call) 8.8   430   110     false(unreach-call) .88  58   13     false(unreach-call) 16    1200 120   disqualified 2.8   84   36    false(unreach-call) .46  62 5.5  false(unreach-call) 14   550 110 false(unreach-call) 14     510   120     false(unreach-call) 22     740   180    
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call error (134) .090 24 .62 false(unreach-call) .15  9.5 1.5  false(unreach-call) .15  9.4 1.5  exception 460   2500 2600 false(unreach-call) 14    79 200   unknown 8.1   430   110     false(unreach-call) 9.0   440   110     false(unreach-call) .88  58   11     false(unreach-call) 16    1300 110   disqualified 3.0   84   37    false(unreach-call) .61  61 6.6  false(unreach-call) 32   550 370 false(unreach-call) 20     560   170     false(unreach-call) 26     750   220    
reducercommutativity/rangesum20_false-unreach-call.i unreach-call error (134) .087 24 .74 false(unreach-call) .53  14   7.8  false(unreach-call) .53  15   7.0  timeout 900   3500 6400 false(unreach-call) 46    94 490   unknown 8.1   430   100     false(unreach-call) 20     490   230     false(unreach-call) 1.4   57   18     false(unreach-call) 18    1300 120   disqualified 3.7   120   50    false(unreach-call) 1.5   62 21    timeout 900   1100 9500 false(unreach-call) 46     970   490     unknown 29     860   250    
reducercommutativity/rangesum40_false-unreach-call.i unreach-call error (134) .085 24 .73 false(unreach-call) .89  24   13    false(unreach-call) 4.2   38   54    timeout 900   5100 6900 unknown 680    270 8000   unknown 8.2   430   88     false(unreach-call) 130     510   1600     false(unreach-call) 9.3   59   110     false(unreach-call) 29    1500 230   disqualified 5.0   140   72    false(unreach-call) 8.4   69 82    timeout 900   1000 11000 timeout 900     1300   9500     unknown 63     920   680    
reducercommutativity/rangesum60_false-unreach-call.i unreach-call error (134) .088 24 .69 false(unreach-call) 5.2   49   67    false(unreach-call) 1.7   42   26    timeout 910   5800 6700 unknown 900    360 11000   unknown 8.4   430   110     false(unreach-call) 190     530   2100     false(unreach-call) 180     170   2200     false(unreach-call) 68    1800 670   disqualified 7.4   220   110    false(unreach-call) 66     89 800    timeout 900   770 10000 timeout 900     3300   11000     unknown 59     1900   560    
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call error (134) .085 24 .94 false(unreach-call) .39  37   5.3  out of memory 350     15000   5600    exception 32   1400 220 false(unreach-call) 4.5  68 54   unknown 8.1   430   100     unknown 1.6   200   23     false(unreach-call) 1.1   58   17     false(unreach-call) 40    1400 400   disqualified 3.7   88   48    false(unreach-call) .76  21 10    false(unreach-call) 12   540 96 timeout 900     1100   10000     false(unreach-call) 27     980   220    
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call error (134) .091 24 .72 error (42) 880     220   13000    error (42) 880     230   13000    timeout 900   2200 7500 unknown 46    84 610   unknown 8.1   430   120     true 8.8   370   120     true 43     70   570     timeout 900    3600 7600   disqualified 2.1   72   26    true .17  18 1.7  timeout 900   760 13000 true 69     760   680     timeout 900     810   13000    
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call error (134) .098 23 .67 error (42) 880     320   13000    error (42) 880     310   13000    timeout 900   3700 10000 unknown 520    200 8200   unknown 8.2   430   94     true 8.5   370   140     true 520     200   7300     timeout 900    3600 8300   disqualified 2.1   76   29    true .17  17 1.8  timeout 900   1600 11000 timeout 900     1400   12000     timeout 900     1900   12000    
reducercommutativity/avg20_true-unreach-call.i unreach-call error (134) .082 24 .84 error (42) 880     470   13000    error (42) 880     410   13000    timeout 900   3800 6300 unknown 900    310 12000   unknown 8.2   430   100     true 8.6   370   110     timeout 900     280   11000     timeout 900    4300 8000   disqualified 2.4   90   34    true .17  18 1.8  timeout 900   5400 7900 timeout 900     4800   8800     timeout 900     5300   6200    
reducercommutativity/avg40_true-unreach-call.i unreach-call error (134) .085 24 .70 error (42) 880     550   11000    error (42) 880     560   12000    timeout 900   6100 6700 unknown 260    270 3000   unknown 8.2   430   110     true 8.8   380   100     timeout 900     360   11000     timeout 900    6000 7600   disqualified 3.3   140   43    true .18  18 2.8  timeout 900   1000 12000 timeout 900     3600   8300     timeout 900     5200   11000    
reducercommutativity/avg60_true-unreach-call.i unreach-call error (134) .079 23 1.0  error (42) 880     650   11000    error (42) 880     670   11000    timeout 900   5100 7300 unknown 900    510 12000   unknown 8.4   430   100     true 8.9   380   120     timeout 900     420   11000     timeout 900    5400 9700   disqualified 5.0   220   70    true .20  17 1.9  timeout 900   890 12000 timeout 900     4000   13000     timeout 900     1600   11000    
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call error (134) .080 24 .70 error (42) 870     360   13000    error (42) 880     310   11000    exception 26   1200 210 unknown 900    130 12000   unknown 8.1   430   110     unknown 1.6   200   18     timeout 900     150   12000     timeout 930    4100 9200   disqualified 880     180   11000    timeout (verification) 900     3800 12000    timeout 900   590 13000 timeout 900     640   12000     timeout 900     700   13000    
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call error (134) .11  24 .66 true 2.1   12   27    true 410     5300   5900    true 220   1500 1700 unknown 2.6  67 39   unknown 8.2   430   97     true 400     410   3900     true .71  28   10     true 240    2300 1900   disqualified 2.1   73   30    true 2.8   23 36    timeout 900   2000 12000 true 440     2600   4800     timeout 900     1300   12000    
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call error (134) .088 24 .75 true 230     49   3500    out of memory 110     15000   1300    timeout 900   2100 6700 unknown 21    68 300   unknown 8.2   430   92     timeout 900     400   7400     true 17     42   220     timeout 900    2900 7200   disqualified 2.4   81   38    true 180     64 2900    timeout 900   2900 8300 timeout 900     5800   10000     timeout 900     1500   13000    
reducercommutativity/max20_true-unreach-call.i unreach-call error (134) .085 24 .82 error (42) 880     210   11000    out of memory 110     15000   1300    timeout 900   2300 7900 unknown 900    140 11000   unknown 8.3   430   120     timeout 900     400   7700     timeout 900     130   13000     timeout 900    2900 6500   disqualified 3.5   110   39    timeout (verification) 900     140 11000    timeout 900   1600 11000 timeout 900     11000   6800     timeout 900     2600   12000    
reducercommutativity/max40_true-unreach-call.i unreach-call error (134) .10  24 .66 error (42) 880     450   12000    out of memory 110     15000   1300    timeout 900   2700 8100 unknown 48    130 690   unknown 8.2   430   100     timeout 900     400   8200     timeout 900     200   13000     timeout 900    2900 11000   disqualified 12     200   100    timeout (verification) 900     200 13000    timeout 900   1400 8400 timeout 900     6500   11000     timeout 900     2200   11000    
reducercommutativity/max60_true-unreach-call.i unreach-call error (134) .11  24 .69 error (42) 880     580   10000    out of memory 110     15000   1500    timeout 900   3000 7600 unknown 160    220 2200   unknown 8.4   430   110     timeout 900     400   8300     timeout 900     240   13000     timeout 900    3400 7900   disqualified 38     340   270    timeout (verification) 900     210 12000    timeout 900   1100 11000 timeout 900     6800   8500     timeout 900     2800   11000    
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call error (134) .086 24 .65 error (42) 880     250   10000    out of memory 410     15000   5300    timeout 960   5400 7300 unknown 900    110 12000   unknown 8.2   430   100     unknown 1.6   200   19     timeout 900     120   11000     timeout 960    4600 6800   disqualified 880     380   11000    error(unknown, verification-finished) 810     3300 9700    timeout 900   4600 7600 timeout 900     3200   7700     timeout 900     4700   6500    
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call error (134) .087 24 .71 true .17  9.9 2.3  error (42) 880     4800   8000    true 290   2500 2800 unknown 2.0  68 26   unknown 8.4   430   120     true 60     390   590     true .19  28   2.2   true 16    1100 120   disqualified 2.1   72   25    true .17  17 1.9  timeout 900   2200 13000 timeout 900     4700   8600     timeout 900     1400   9900    
reducercommutativity/sep10_true-unreach-call.i unreach-call error (134) .087 23 .70 true .38  15   5.9  out of memory 110     15000   1500    exception 80   2500 820 unknown 4.3  67 62   unknown 8.3   430   110     timeout 900     430   6900     true .20  28   2.7   true 31    1400 350   disqualified 3.0   81   39    true .21  16 1.8  timeout 900   5600 9300 timeout 900     4800   8300     timeout 900     5400   9200    
reducercommutativity/sep20_true-unreach-call.i unreach-call error (134) .10  24 .69 true 4.9   35   79    out of memory 110     15000   1200    timeout 910   4800 8900 unknown 12    67 160   unknown 8.4   430   100     timeout 900     400   7100     true .24  28   2.3   true 240    1900 1800   disqualified 880     110   12000    true .22  17 2.0  timeout 900   4200 7800 timeout 900     12000   9000     timeout 900     4300   9500    
reducercommutativity/sep40_true-unreach-call.i unreach-call error (134) .10  24 .83 true 37     85   460    out of memory 110     15000   1400    timeout 910   3500 9100 unknown 41    87 550   unknown 8.3   430   100     timeout 900     400   7300     true .26  28   3.2   timeout 900    2800 8200   disqualified 880     170   12000    true .19  18 1.8  timeout 900   1200 10000 timeout 900     13000   8300     timeout 900     2000   10000    
reducercommutativity/sep60_true-unreach-call.i unreach-call error (134) .11  24 .69 true 170     160   2200    out of memory 110     15000   1300    timeout 920   4400 11000 unknown 98    180 1400   unknown 8.2   430   93     timeout 900     410   7600     true .33  29   4.4   timeout 900    3600 6600   disqualified 880     270   13000    true .18  18 2.0  timeout 900   1100 11000 timeout 910     13000   9700     timeout 900     2200   10000    
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call error (134) .11  24 .78 error (42) 880     810   7000    out of memory 570     15000   8900    timeout 940   5000 9600 unknown 900    88 12000   unknown 8.1   430   110     unknown 1.6   200   20     timeout 900     120   10000     timeout 910    3200 8800   disqualified 880     180   11000    error(unknown, verification-finished) 800     3100 9200    timeout 900   2100 11000 timeout 900     830   12000     timeout 900     1500   10000    
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call error (134) .088 24 .80 true 34     21   430    true 45     23   700    timeout 900   1600 12000 unknown 2.0  66 24   unknown 8.2   430   100     true 8.4   370   110     true .17  27   2.0   timeout 900    2200 10000   disqualified 2.1   73   23    true .17  17 1.9  timeout 900   4700 6900 true 700     800   10000     timeout 900     4100   6600    
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call error (134) .081 24 .83 error (42) 880     250   11000    error (42) 870     250   12000    timeout 900   3600 6600 unknown 4.0  67 51   unknown 8.3   430   130     true 8.5   370   97     true .17  27   2.3   timeout 900    4300 6400   disqualified 2.1   76   26    true .19  17 1.6  timeout 900   1200 11000 timeout 900     4900   6800     timeout 900     1200   13000    
reducercommutativity/sum20_true-unreach-call.i unreach-call error (134) .088 23 .73 error (42) 870     410   13000    error (42) 880     430   11000    timeout 900   4700 6800 unknown 10    69 130   unknown 8.1   430   96     true 8.6   370   98     true .19  27   2.9   timeout 900    4200 6600   disqualified 2.3   90   33    true .17  17 2.2  timeout 900   5300 7600 timeout 900     5400   6300     timeout 900     5400   6900    
reducercommutativity/sum40_true-unreach-call.i unreach-call error (134) .082 24 .90 error (42) 880     560   14000    error (42) 870     550   11000    timeout 910   5600 8200 unknown 36    75 460   unknown 8.5   430   100     true 8.6   370   100     true .23  27   3.2   timeout 900    6800 7500   disqualified 2.8   140   35    true .18  17 2.0  timeout 900   1100 11000 timeout 900     6100   6100     timeout 900     3500   12000    
reducercommutativity/sum60_true-unreach-call.i unreach-call error (134) .082 24 .77 error (42) 880     620   11000    error (42) 880     600   9800    timeout 910   6300 7700 unknown 900    800 11000   unknown 8.2   430   110     true 8.4   380   110     true .30  27   3.2   timeout 910    5300 6700   disqualified 4.8   220   61    true .20  17 2.2  timeout 900   1100 9400 timeout 900     3600   12000     timeout 900     1600   12000    
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call error (134) .088 23 .85 error (42) 880     360   10000    error (42) 880     1000   13000    timeout 970   4500 9500 unknown 890    120 9800   unknown 7.9   430   100     unknown 1.6   200   19     timeout 900     160   13000     timeout 970    4500 9100   disqualified 880     380   10000    error(unknown, verification-finished) 890     3400 9300    timeout 900   770 12000 timeout 900     4800   7800     timeout 900     14000   6000    
array-tiling/mlceu_false-unreach-call.i unreach-call out of memory 790     15000 3900    out of memory 520     13000   6700    error (42) 870     4400   9700    timeout 960   5600 9300 unknown 900    84 14000   unknown 8.1   430   86     unknown 1.6   200   21     timeout 900     140   11000     timeout 960    5900 7000   disqualified 880     270   7800    timeout (verification) 900     1300 9400    timeout 900   1500 11000 timeout 900     840   6700     timeout 900     1400   11000    
array-tiling/skippedu_false-unreach-call.i unreach-call false(unreach-call) .30  27 3.2  false(unreach-call) .088 9.7 .96 false(unreach-call) .11  9.5 1.1  false(unreach-call) 6.4 320 60 false(unreach-call) .38 35 4.9 unknown 8.4   430   100     unknown 1.5   200   18     false(unreach-call) .10  26   1.2   false(unreach-call) 16    1200 110   disqualified 3.2   82   37    timeout (verification) 900     420 15000    false(unreach-call) 9.8 410 83 false(unreach-call) 9.1   370   67     false(unreach-call) 11     500   97    
array-tiling/mbpr2_true-unreach-call.i unreach-call out of memory 490     15000 2700    out of memory 99     13000   1200    out of memory 800     15000   11000    timeout 970   6000 7500 unknown 900    100 10000   unknown 8.4   430   99     unknown 1.6   200   22     timeout 900     150   10000     timeout 960    5100 7500   disqualified 880     390   11000    timeout (verification) 900     380 11000    timeout 900   920 11000 timeout 900     960   7800     timeout 900     790   12000    
array-tiling/mbpr3_true-unreach-call.i unreach-call out of memory 340     15000 2900    out of memory 210     13000   2900    out of memory 630     15000   7200    timeout 960   6700 7200 unknown 900    280 10000   unknown 8.3   430   110     unknown 1.6   200   23     timeout 900     160   9900     timeout 970    7100 9000   disqualified 880     410   8100    timeout (verification) 900     280 13000    timeout 900   930 13000 timeout 900     1400   8600     timeout 900     990   11000    
array-tiling/mbpr4_true-unreach-call.i unreach-call out of memory 310     15000 3000    error (134) 430     14000   5400    out of memory 500     15000   6800    timeout 920   7500 9100 unknown 900    86 11000   unknown 8.1   430   110     unknown 1.6   200   19     timeout 900     170   11000     timeout (exception) 910    7200 9800   disqualified 880     500   9000    timeout (verification) 900     350 11000    timeout 900   900 11000 timeout 900     1000   6800     timeout 900     850   12000    
array-tiling/mbpr5_true-unreach-call.i unreach-call timeout 900     12000 5300    error (134) 780     14000   9900    out of memory 450     15000   5500    timeout 930   7200 9500 unknown 900    320 12000   unknown 8.2   430   100     unknown 1.6   200   20     timeout 900     170   11000     timeout 930    7500 8700   disqualified 880     510   9200    timeout (verification) 900     270 12000    timeout 900   1200 10000 timeout 900     1000   9000     timeout 900     1600   10000    
array-tiling/nr2_true-unreach-call.i unreach-call out of memory 390     15000 2000    error (42) 880     12000   11000    out of memory 300     15000   4400    timeout 970   6700 10000 unknown 900    680 12000   unknown 8.2   430   100     unknown 1.5   200   18     timeout 900     140   12000     timeout 960    4400 9700   disqualified 880     330   14000    timeout (verification) 900     410 12000    timeout 900   1100 15000 timeout 900     930   7900     timeout 900     1100   9400    
array-tiling/nr3_true-unreach-call.i unreach-call out of memory 770     15000 2800    out of memory 91     13000   970    out of memory 400     15000   5200    timeout 960   6200 7800 unknown 900    660 9800   unknown 8.1   430   110     unknown 1.6   200   20     timeout 900     140   13000     timeout 970    6500 8800   disqualified 880     360   10000    timeout (verification) 900     320 11000    timeout 900   1000 13000 timeout 900     1000   9000     timeout 900     1600   12000    
array-tiling/nr4_true-unreach-call.i unreach-call out of memory 350     15000 2000    out of memory 120     14000   1800    out of memory 510     15000   7500    timeout 970   6600 8500 unknown 900    630 12000   unknown 8.1   430   110     unknown 1.6   200   20     timeout 900     140   12000     timeout 960    5200 8200   disqualified 880     380   12000    timeout (verification) 900     390 12000    timeout 900   2100 12000 timeout 900     940   10000     timeout 900     1900   10000    
array-tiling/nr5_true-unreach-call.i unreach-call out of memory 390     15000 2100    error (134) 150     14000   1800    out of memory 690     15000   11000    timeout 960   6100 11000 unknown 900    590 13000   unknown 8.3   430   99     unknown 1.6   200   19     timeout 900     130   12000     timeout 960    5100 8100   disqualified 880     410   9300    timeout (verification) 900     290 11000    timeout 900   2200 14000 timeout 900     980   7400     timeout 900     2100   11000    
array-tiling/pnr2_true-unreach-call.i unreach-call out of memory 780     15000 3200    out of memory 120     13000   1300    out of memory 550     15000   6500    timeout 960   3700 9700 unknown 900    220 11000   unknown 8.3   430   86     unknown 1.6   200   21     timeout 900     240   9200     timeout 970    3300 8300   disqualified 880     210   11000    timeout (verification) 900     400 11000    timeout 900   1300 11000 timeout 900     990   7000     timeout 900     5400   8000    
array-tiling/pnr3_true-unreach-call.i unreach-call out of memory 590     15000 3000    out of memory 210     13000   3000    out of memory 220     15000   3000    timeout 960   6900 7100 unknown 900    210 8900   unknown 8.2   430   110     unknown 1.6   200   18     timeout 900     280   11000     timeout 960    6500 7600   disqualified 880     220   11000    timeout (verification) 900     310 12000    timeout 900   1500 12000 timeout 900     1300   10000     timeout 900     1000   13000    
array-tiling/pnr4_true-unreach-call.i unreach-call out of memory 660     15000 3600    out of memory 350     13000   3600    out of memory 190     15000   2900    timeout 960   3500 10000 unknown 890    280 14000   unknown 8.1   430   97     unknown 1.6   200   21     timeout 900     270   9800     timeout 970    3100 8200   disqualified 880     260   10000    timeout (verification) 900     380 14000    timeout 900   1100 10000 timeout 900     2400   11000     timeout 900     1200   11000    
array-tiling/pnr5_true-unreach-call.i unreach-call out of memory 490     15000 2100    out of memory 520     13000   5600    out of memory 210     15000   2500    timeout 960   6600 9300 unknown 900    430 10000   unknown 8.3   430   99     unknown 1.6   200   19     timeout 900     260   12000     timeout 960    6100 8900   disqualified 880     250   11000    timeout (verification) 900     280 14000    timeout 900   5000 13000 timeout 900     3900   10000     timeout 900     1600   12000    
array-tiling/poly1_true-unreach-call.i unreach-call timeout 900     10000 5700    out of memory 74     14000   960    error (42) 880     4200   12000    timeout 960   5300 6100 unknown 10    38 170   unknown 8.2   430   93     unknown 1.5   200   17     unknown .076 26   .80  timeout 900    1700 11000   disqualified 880     180   11000    timeout (verification) 900     580 11000    timeout 900   750 11000 timeout 900     1100   10000     timeout 900     610   10000    
array-tiling/poly2_true-unreach-call.i unreach-call timeout 900     8600 4500    out of memory 100     14000   1200    error (42) 880     8600   14000    timeout 970   5100 6600 unknown 13    39 190   unknown 8.1   430   120     unknown 1.5   200   20     unknown .099 26   .81  timeout 950    5400 7300   disqualified 880     700   12000    timeout (verification) 900     500 12000    timeout 900   630 13000 timeout 900     980   11000     timeout 900     710   14000    
array-tiling/pr2_true-unreach-call.i unreach-call out of memory 610     15000 2700    out of memory 120     13000   1300    out of memory 260     15000   3200    timeout 960   3800 6800 unknown 900    130 12000   unknown 8.3   430   110     unknown 1.6   200   22     timeout 900     180   13000     timeout 960    4000 6800   disqualified 880     380   11000    timeout (verification) 900     1500 12000    timeout 900   1600 12000 timeout 900     920   8500     timeout 900     2100   10000    
array-tiling/pr3_true-unreach-call.i unreach-call out of memory 370     15000 2000    out of memory 220     13000   2400    out of memory 150     15000   2100    timeout 960   3800 6400 unknown 900    190 13000   unknown 8.1   430   110     unknown 1.6   200   22     timeout 900     200   11000     timeout 960    4100 7000   disqualified 880     370   10000    timeout (verification) 900     1400 13000    timeout 900   1100 11000 timeout 900     930   8300     timeout 900     950   10000    
array-tiling/pr4_true-unreach-call.i unreach-call out of memory 400     15000 2200    out of memory 350     13000   4500    out of memory 150     15000   2200    timeout 960   3800 7000 unknown 900    120 13000   unknown 8.3   430   110     unknown 1.6   200   20     timeout 900     200   11000     timeout 960    3800 7800   disqualified 880     390   11000    timeout (verification) 900     1700 10000    timeout 900   990 12000 timeout 900     900   11000     timeout 900     910   9200    
array-tiling/pr5_true-unreach-call.i unreach-call out of memory 310     15000 2400    out of memory 520     13000   6400    out of memory 210     15000   2600    timeout 960   3300 8900 unknown 900    160 13000   unknown 8.3   430   110     unknown 1.5   200   20     timeout 900     230   13000     timeout 960    3500 8500   disqualified 880     400   10000    timeout (verification) 900     1400 10000    timeout 900   1100 9100 timeout 900     870   9500     timeout 900     1100   12000    
array-tiling/revcpyswp2_true-unreach-call.i unreach-call timeout 900     11000 4800    out of memory 210     14000   2300    error (42) 870     2000   12000    timeout 960   3400 6400 unknown 900    100 11000   unknown 8.3   430   100     unknown 1.6   200   18     timeout 900     190   12000     timeout 960    3400 8100   disqualified 880     290   14000    timeout (verification) 900     140 13000    timeout 900   940 12000 timeout 900     1000   8200     timeout 900     830   10000    
array-tiling/rew_true-unreach-call.i unreach-call out of memory 770     15000 3700    error (42) 880     9300   12000    out of memory 490     15000   6400    timeout 960   4100 7200 unknown 900    98 13000   unknown 8.2   430   97     unknown 1.6   200   22     timeout 900     170   11000     timeout 970    4100 7400   disqualified 880     390   11000    timeout (verification) 900     920 11000    timeout 900   1500 12000 timeout 900     990   7300     timeout 900     1100   12000    
array-tiling/rewnif_true-unreach-call.i unreach-call out of memory 680     15000 5500    error (42) 880     9300   13000    out of memory 510     15000   7000    timeout 960   4200 7700 unknown 900    98 10000   unknown 8.1   430   120     unknown 1.6   200   25     timeout 900     160   11000     timeout 960    5300 6900   disqualified 880     400   12000    timeout (verification) 900     920 12000    timeout 900   1200 10000 timeout 900     900   6300     timeout 900     950   11000    
array-tiling/rewnifrev2_true-unreach-call.i unreach-call out of memory 710     15000 4400    out of memory 170     13000   2200    error (42) 880     1600   9600    timeout 960   4100 9500 unknown 900    220 11000   unknown 8.2   430   110     unknown 1.6   200   23     timeout 900     330   13000     timeout 970    3400 8700   disqualified 880     310   10000    timeout (verification) 900     570 12000    timeout 900   2400 12000 timeout 900     800   7100     timeout 900     2400   11000    
array-tiling/rewnifrev_true-unreach-call.i unreach-call out of memory 730     15000 3200    out of memory 220     12000   2500    error (42) 880     1200   13000    timeout 960   3900 7200 unknown 900    210 14000   unknown 8.2   430   94     unknown 1.5   200   19     timeout 900     340   11000     timeout 960    4100 7700   disqualified 880     320   11000    timeout (verification) 900     600 13000    timeout 900   1100 9300 timeout 900     980   6900     timeout 900     980   8900    
array-tiling/rewrev_true-unreach-call.i unreach-call out of memory 640     15000 2900    out of memory 220     12000   2400    error (42) 880     1300   10000    timeout 960   4100 7100 unknown 900    150 11000   unknown 8.0   430   100     unknown 1.6   200   19     timeout 900     240   13000     timeout 960    5000 7700   disqualified 880     280   12000    timeout (verification) 900     660 11000    timeout 900   1200 11000 timeout 900     1100   8300     timeout 900     1400   11000    
array-tiling/skipped_true-unreach-call.i unreach-call out of memory 900     15000 5000    out of memory 100     14000   1500    out of memory 580     15000   8500    timeout 960   3700 10000 unknown 900    390 11000   unknown 8.2   430   110     unknown 1.6   200   23     timeout 900     250   12000     timeout 970    4300 9400   disqualified 880     230   13000    timeout (verification) 900     420 13000    timeout 900   2600 11000 timeout 900     1000   8300     timeout 900     2700   11000    
array-tiling/tcpy_true-unreach-call.i unreach-call timeout 900     10000 3800    error (42) 880     11000   5500    error (42) 880     2500   10000    timeout 960   3700 9700 unknown 900    130 14000   unknown 8.3   430   110     unknown 1.6   200   19     timeout 900     170   10000     timeout 960    3000 7700   disqualified 880     240   14000    timeout (verification) 900     690 12000    timeout 900   1300 11000 timeout 900     900   8200     timeout 900     2400   8000    
array-programs/copysome1_false-unreach-call.i unreach-call error (134) .083 24 .86 out of memory 160     15000   2100    error (42) 880     5400   12000    timeout 970   4600 11000 unknown 220    120 3100   timeout 900     440   9800     timeout 900     3300   7800     timeout 900     11000   9400     timeout 970    6200 9600   disqualified 880     820   13000    false(unreach-call) 25     1200 240    timeout 900   1500 12000 timeout 900     4100   8000     timeout 900     3700   11000    
array-programs/copysome2_false-unreach-call.i unreach-call error (134) .083 24 .81 out of memory 150     15000   2100    error (42) 880     8600   12000    timeout 960   4100 10000 unknown 350    95 4600   timeout 900     430   8100     timeout 900     3300   8600     timeout 900     11000   11000     timeout 900    9100 11000   disqualified 890     860   13000    false(unreach-call) 42     1500 370    timeout 900   1600 8400 timeout 900     5000   9400     timeout 900     1700   13000    
array-programs/copysome1_true-unreach-call.i unreach-call error (134) .093 24 .79 out of memory 160     15000   2000    error (42) 880     5400   11000    timeout 960   5000 9300 unknown 230    67 2700   timeout 900     440   8900     timeout 900     3300   8100     timeout 900     11000   9500     timeout 970    6500 8300   disqualified 880     790   11000    true 17     770 130    timeout 900   1600 9800 timeout 900     5100   8400     timeout 900     4100   13000    
array-programs/copysome2_true-unreach-call.i unreach-call error (134) .081 24 .76 out of memory 150     15000   2200    error (42) 880     8600   12000    timeout 970   5100 9200 unknown 280    84 3800   timeout 900     430   9400     timeout 900     3300   10000     timeout 900     11000   9400     timeout 900    8200 12000   disqualified 890     820   11000    true 31     1100 220    timeout 900   1600 7800 timeout 900     5100   7700     timeout 900     1900   11000    
array-crafted/bAnd1_true-unreach-call.i unreach-call error (134) .095 24 .64 true .59  29   7.3  true .62  31   7.8  timeout 900   6500 8100 unknown 240    240 3000   unknown 8.3   430   110     true 8.8   380   110     true .68  29   9.8   timeout 900    5100 8000   disqualified 880     1700   7400    true .18  18 2.0  timeout 900   980 11000 timeout 900     3700   10000     timeout 900     1500   14000    
array-crafted/bAnd2_true-unreach-call.i unreach-call error (134) .079 23 .79 true 9.0   1200   120    true 8.7   1200   120    timeout 910   5900 11000 unknown 220    180 2600   unknown 10     450   110     true 26     600   280     true 17     290   220     timeout 910    6500 8200   disqualified 66     15000   590    true 23     180 200    timeout 900   1000 11000 timeout 900     5700   10000     timeout 900     1400   11000    
array-crafted/bAnd3_true-unreach-call.i unreach-call error (134) .086 24 .72 out of memory 71     15000   1100    out of memory 62     15000   910    timeout 960   5400 9900 unknown 210    170 3100   unknown 33     680   370     timeout 900     1300   8100     timeout 900     11000   10000     timeout 970    6600 8500   disqualified 880     490   13000    timeout (verification) 900     1700 6700    timeout 900   1000 10000 timeout 900     5300   9100     timeout 900     1400   13000    
array-crafted/bAnd4_true-unreach-call.i unreach-call error (134) .082 24 .89 out of memory 53     15000   660    out of memory 50     15000   660    timeout 960   4000 8900 unknown 280    220 3500   timeout 900     2300   10000     timeout 900     2300   9200     timeout 900     11000   12000     timeout 960    4700 8400   disqualified 3.9   100   48    out of memory (killed (signal 9, verification)) 560     15000 3300    timeout 900   850 9400 timeout 900     6200   8300     timeout 900     1300   11000    
array-crafted/bAnd5_true-unreach-call.i unreach-call error (134) .084 23 .70 error (42) 880     8500   4100    error (42) 870     1500   11000    timeout 960   4600 7200 unknown 900    86 11000   unknown 8.2   430   100     unknown 1.6   200   21     timeout 900     170   13000     timeout 970    4600 8100   disqualified 880     400   8700    error(unknown, verification-finished) 860     3400 10000    timeout 900   950 11000 timeout 900     830   11000     timeout 900     1200   12000    
array-crafted/bor1_true-unreach-call.i unreach-call error (134) .088 24 .63 true .62  29   8.1  true .61  31   8.6  timeout 910   7600 8100 unknown 170    97 2500   unknown 8.4   430   97     true 8.8   380   100     true .46  28   5.7   timeout 900    5900 7600   disqualified 880     1000   8900    true .17  18 2.7  timeout 900   1000 10000 timeout 900     4500   9300     timeout 900     1700   11000    
array-crafted/bor2_true-unreach-call.i unreach-call error (134) .086 23 .65 true 8.9   1200   120    true 8.7   1200   100    timeout 910   5900 9700 unknown 190    98 3100   unknown 9.8   450   130     true 25     600   280     true 16     280   200     timeout 910    6300 8500   disqualified 65     15000   610    true 10     110 120    timeout 900   850 9700 timeout 900     5200   11000     timeout 900     1300   11000    
array-crafted/bor3_true-unreach-call.i unreach-call error (134) .089 24 .52 out of memory 71     15000   990    out of memory 62     15000   1000    timeout 970   4800 10000 unknown 180    100 2300   unknown 33     680   370     timeout 900     1300   7900     timeout 900     11000   10000     timeout 960    6200 8300   disqualified 880     340   9500    true 520     1300 5000    timeout 900   1100 8700 timeout 900     5400   7500     timeout 900     1400   12000    
array-crafted/bor4_true-unreach-call.i unreach-call error (134) .10  24 .79 out of memory 53     15000   800    out of memory 50     15000   630    timeout 960   4300 10000 unknown 230    100 3300   timeout 900     2300   10000     timeout 900     2300   9400     timeout 900     11000   10000     timeout 960    7300 8700   disqualified 62     120   870    out of memory (killed (signal 9, verification)) 180     15000 1500    timeout 900   1100 9500 timeout 900     5300   8100     timeout 900     1400   11000    
array-crafted/bor5_true-unreach-call.i unreach-call error (134) .082 24 .83 error (42) 880     8500   3500    error (42) 870     1500   10000    timeout 960   4700 7600 unknown 900    85 11000   unknown 8.3   430   110     unknown 1.6   200   23     timeout 900     160   11000     timeout 960    5400 7500   disqualified 880     330   8500    error(unknown, verification-finished) 870     3500 10000    timeout 900   1100 13000 timeout 900     820   12000     timeout 900     880   13000    
array-crafted/mapavg1_true-unreach-call.i unreach-call error (134) .082 24 .71 error (42) 880     730   9000    error (42) 880     700   8800    timeout 900   5300 7500 unknown 900    180 10000   unknown 8.4   430   97     true 9.1   390   140     timeout 900     430   9900     timeout 900    5500 8300   disqualified 13     460   150    true .19  17 2.2  timeout 900   1100 8600 timeout 900     4900   11000     timeout 900     1900   12000    
array-crafted/mapavg2_true-unreach-call.i unreach-call error (134) .082 24 .81 error (42) 880     2600   7500    error (42) 880     2800   7500    timeout 920   7800 8500 unknown 900    170 11000   unknown 9.8   440   130     timeout 900     1500   9000     timeout 900     1500   11000     timeout 920    6500 7800   disqualified 890     8400   2700    timeout (verification) 900     710 8900    timeout 900   900 13000 timeout 900     6400   8800     timeout 900     1400   12000    
array-crafted/mapavg3_true-unreach-call.i unreach-call error (134) .087 23 .85 out of memory 73     15000   1000    out of memory 64     15000   920    timeout 960   4600 11000 unknown 900    200 11000   unknown 33     680   390     timeout 900     1300   8500     timeout 900     11000   9400     timeout 960    6200 8600   disqualified 890     690   9700    timeout (verification) 900     4700 5500    timeout 900   1100 9700 timeout 900     5200   8500     timeout 900     1400   11000    
array-crafted/mapavg4_true-unreach-call.i unreach-call error (134) .086 24 .77 out of memory 53     15000   790    out of memory 50     15000   710    timeout 960   3700 11000 unknown 900    190 11000   timeout 900     2300   12000     timeout 900     2300   9200     timeout 900     12000   10000     timeout 970    5900 9800   disqualified 2.2   80   26    timeout (verification) 900     300 7800    timeout 900   1100 9400 timeout 900     6600   9800     timeout 900     1600   12000    
array-crafted/mapavg5_true-unreach-call.i unreach-call error (134) .12  24 .76 error (42) 880     240   10000    error (42) 880     200   12000    exception 11   660 92 unknown 900    130 10000   unknown 8.4   430   97     unknown 1.6   200   19     timeout 900     140   13000     timeout 900    2800 7100   disqualified 880     430   12000    timeout (verification) 900     3700 11000    timeout 900   710 11000 timeout 900     850   13000     timeout 900     2100   13000    
array-crafted/mapsum1_true-unreach-call.i unreach-call error (134) .12  24 .75 error (42) 880     680   11000    error (42) 880     660   11000    timeout 910   6500 9100 unknown 900    200 11000   unknown 8.4   430   99     true 8.6   380   110     true .50  29   6.3   timeout 910    6100 7100   disqualified 17     470   180    true .18  17 2.1  timeout 900   1000 12000 timeout 900     5800   13000     timeout 900     1700   13000    
array-crafted/mapsum2_true-unreach-call.i unreach-call error (134) .084 24 .81 error (42) 880     2900   8400    error (42) 880     2900   8600    timeout 910   6000 9900 unknown 900    280 12000   unknown 9.9   450   120     true 25     700   260     true 18     300   230     timeout 920    6600 9300   disqualified 880     8400   3200    true .66  36 11    timeout 900   2000 10000 timeout 900     5900   8200     timeout 900     1500   13000    
array-crafted/mapsum3_true-unreach-call.i unreach-call error (134) .083 24 .74 out of memory 73     15000   890    out of memory 64     15000   850    timeout 960   5500 10000 unknown 900    220 11000   unknown 33     680   440     timeout 900     1300   8300     timeout 900     11000   9300     timeout 970    6000 8600   disqualified 890     700   12000    true 56     1300 870    timeout 900   830 9000 timeout 900     5400   8100     timeout 900     1500   11000    
array-crafted/mapsum4_true-unreach-call.i unreach-call error (134) .087 24 .63 out of memory 53     15000   780    out of memory 50     15000   660    timeout 970   5000 11000 unknown 900    220 11000   timeout 900     2300   9400     timeout 900     2300   8800     timeout 900     12000   12000     timeout 970    6900 8200   disqualified 2.2   77   25    timeout (verification) 900     370 8100    timeout 900   1100 9800 timeout 900     5400   10000     timeout 900     1400   12000    
array-crafted/mapsum5_true-unreach-call.i unreach-call error (134) .10  24 .68 error (42) 880     210   9800    error (42) 880     190   12000    timeout 960   3900 9800 unknown 900    140 11000   unknown 8.1   430   120     unknown 1.5   200   21     timeout