Tool 2LS 0.5.0 BLAST 2.7.3 CBMC 5.6 Ceagle Ceagle 1.3 @ 53cfa89 CPAchecker 1.6.1-svn 23987 CPAchecker 1.6.1-svn 24048 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 3.1 64-bit x86_64 linux SMACK+Corral 1.7.2 symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a ULTIMATE Automizer f7c3ed31 ULTIMATE Kojak f7c3ed31 ULTIMATE Taipan f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-generic [Linux 4.4.0-57-generic; Linux 4.4.0-59-generic] Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:51:44 CET ]] [[ 2017-01-14 18:06:48 CET ]] [[ 2017-01-14 19:59:41 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:52:12 CET ]] [[ 2017-01-14 18:07:02 CET ]] [[ 2017-01-14 19:59:19 CET ]] 2017-01-10 20:44:08 CET [[ 2017-01-14 18:01:01 CET ]] [[ 2017-01-14 20:09:29 CET ]] [[ 2017-01-14 18:26:00 CET ]] [[ 2017-01-14 20:41:28 CET ]] 2017-01-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]] 2017-01-11 11:18:39 CET [[ 2017-01-14 21:32:33 CET ]] [[ 2017-01-14 22:21:46 CET ]] [[ 2017-01-14 21:35:07 CET ]] [[ 2017-01-14 22:35:09 CET ]] 2017-01-11 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]] 2017-01-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]] 2017-01-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]] 2017-01-11 16:16:17 CET [[ 2017-01-14 22:37:08 CET ]] [[ 2017-01-15 00:13:18 CET ]] [[ 2017-01-14 22:52:42 CET ]] [[ 2017-01-15 00:24:59 CET ]] 2017-01-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]] 2017-01-13 11:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]] 2017-01-13 11:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]] 2017-01-13 12:41:58 CET [[ 2017-01-15 02:09:41 CET ]] [[ 2017-01-15 04:03:21 CET ]] [[ 2017-01-15 02:31:54 CET ]] [[ 2017-01-15 04:27:36 CET ]] 2017-01-13 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]] 2017-01-14 09:46:18 CET [[ 2017-01-15 02:18:39 CET ]] [[ 2017-01-15 04:12:25 CET ]] [[ 2017-01-15 02:37:40 CET ]] [[ 2017-01-15 04:38:18 CET ]]
Run set 2ls.sv-comp17.ReachSafety-Floats blast.sv-comp17.ReachSafety-Floats cbmc.sv-comp17.ReachSafety-Floats ceagle.sv-comp17.ReachSafety-Floats cpa-bam-bnb.sv-comp17.ReachSafety-Floats cpa-kind.sv-comp17.ReachSafety-Floats cpa-seq.sv-comp17.ReachSafety-Floats depthk.sv-comp17.ReachSafety-Floats esbmc.sv-comp17.ReachSafety-Floats esbmc-falsi.sv-comp17.ReachSafety-Floats esbmc-incr.sv-comp17.ReachSafety-Floats esbmc-kind.sv-comp17.ReachSafety-Floats smack.sv-comp17.ReachSafety-Floats symbiotic4.sv-comp17.ReachSafety-Floats uautomizer.sv-comp17.ReachSafety-Floats ukojak.sv-comp17.ReachSafety-Floats utaipan.sv-comp17.ReachSafety-Floats
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
floats-cdfpl/newton_1_4_false-unreach-call.i false(unreach-call) 14     62 160    1 timeout 900     25   13000    0 false(unreach-call) 4.2  59 41    1 false(unreach-call) 42     550   460    1 false(unreach-call) 31   1100 270 1 false(unreach-call) 200   3000 880 1 false(unreach-call) 32   330 210 1 unknown 890    470 8200   0 false(unreach-call) 35    200 310   1 timeout 900     470 9400    0 timeout 900     470 8100    0 timeout 900     470 7000    0 error (1) 890     580   7200    0 unknown .14  9.4 1.7  0 false(unreach-call) 100   3900 830 1 error 85   1100 730 0 false(unreach-call) 100   3900 720 1
floats-cdfpl/newton_1_5_false-unreach-call.i false(unreach-call) 13     57 150    1 timeout 900     25   12000    0 false(unreach-call) 4.0  61 53    1 false(unreach-call) 31     560   270    1 false(unreach-call) 9.4 580 83 1 false(unreach-call) 67   750 350 1 false(unreach-call) 48   330 380 1 unknown 890    480 6700   0 false(unreach-call) 19    180 110   1 timeout 900     480 8300    0 timeout 900     480 7900    0 timeout 900     480 7300    0 false(unreach-call) 490     530   4000    1 unknown .16  9.4 1.7  0 false(unreach-call) 65   2200 470 1 error 84   1100 860 0 false(unreach-call) 64   2200 570 1
floats-cdfpl/newton_1_6_false-unreach-call.i false(unreach-call) 11     54 110    1 timeout 900     25   12000    0 false(unreach-call) 3.0  51 29    1 false(unreach-call) 57     560   540    1 false(unreach-call) 5.0 460 54 1 false(unreach-call) 75   660 450 1 false(unreach-call) 11   330 83 1 unknown 890    450 7700   0 false(unreach-call) 8.7  180 81   1 timeout 900     440 7400    0 timeout 900     440 6500    0 timeout 900     440 6600    0 false(unreach-call) 380     540   2700    1 unknown .16  9.4 1.8  0 false(unreach-call) 51   1700 360 1 error 79   1100 580 0 false(unreach-call) 52   1700 420 1
floats-cdfpl/newton_1_7_false-unreach-call.i false(unreach-call) 8.6   48 77    1 timeout 900     25   10000    0 false(unreach-call) 3.6  52 39    1 false(unreach-call) 51     560   630    1 false(unreach-call) 8.8 540 78 1 false(unreach-call) 13   490 92 1 false(unreach-call) 11   330 80 1 unknown 890    470 7500   0 false(unreach-call) 8.2  180 77   1 timeout 900     460 6700    0 timeout 900     380 2500    0 timeout 900     460 6500    0 false(unreach-call) 460     530   4000    1 unknown .17  9.4 1.4  0 false(unreach-call) 68   2100 570 1 error 82   1000 810 0 false(unreach-call) 66   2000 520 1
floats-cdfpl/newton_1_8_false-unreach-call.i false(unreach-call) 5.6   52 59    1 timeout 900     25   12000    0 false(unreach-call) 4.1  60 46    1 false(unreach-call) 23     560   210    1 false(unreach-call) 6.1 480 60 1 false(unreach-call) 55   920 330 1 false(unreach-call) 12   330 95 1 false(unreach-call) 880    460 8400   1 false(unreach-call) 14    190 130   1 false(unreach-call) 880     460 7700    1 false(unreach-call) 870     460 8100    1 timeout 900     450 7100    0 false(unreach-call) 250     500   2200    1 unknown .17  9.2 1.8  0 false(unreach-call) 28   980 290 1 error 80   1000 840 0 false(unreach-call) 27   980 210 1
floats-cdfpl/newton_2_6_false-unreach-call.i false(unreach-call) 98     190 1300    1 timeout 900     25   13000    0 false(unreach-call) 31    130 330    1 false(unreach-call) 120     1900   1100    1 false(unreach-call) 29   1100 230 1 false(unreach-call) 410   5100 1900 1 false(unreach-call) 40   420 250 1 unknown 890    760 6900   0 false(unreach-call) 26    360 220   1 timeout 900     760 7200    0 timeout 900     750 6800    0 timeout 900     760 5800    0 error (1) 890     930   7800    0 unknown .16  9.3 1.7  0 out of memory 420   15000 2800 0 error 70   1400 650 0 out of memory 420   15000 2800 0
floats-cdfpl/newton_2_7_false-unreach-call.i false(unreach-call) 87     180 740    1 timeout 900     25   10000    0 false(unreach-call) 15    120 160    1 false(unreach-call) 82     1900   660    1 false(unreach-call) 10   660 95 1 false(unreach-call) 250   1900 1300 1 false(unreach-call) 40   430 300 1 unknown 890    760 6800   0 false(unreach-call) 17    350 170   1 timeout 900     760 7300    0 timeout 900     760 8700    0 timeout 900     750 6800    0 error (1) 890     990   6900    0 unknown .17  9.3 1.6  0 false(unreach-call) 170   5000 1600 1 error 67   1400 590 0 false(unreach-call) 170   4900 1200 1
floats-cdfpl/newton_2_8_false-unreach-call.i false(unreach-call) 110     190 940    1 timeout 900     25   12000    0 false(unreach-call) 21    130 230    1 false(unreach-call) 76     1900   620    1 false(unreach-call) 87   2400 610 1 false(unreach-call) 550   1200 4000 1 false(unreach-call) 13   430 100 1 unknown 890    760 6500   0 false(unreach-call) 11    350 130   1 timeout 900     760 8000    0 timeout 900     760 9400    0 timeout 900     760 7600    0 error (1) 890     980   7200    0 unknown .17  9.4 1.6  0 false(unreach-call) 110   2900 760 1 error 75   1400 690 0 false(unreach-call) 110   2800 760 1
floats-cdfpl/newton_3_6_false-unreach-call.i false(unreach-call) 630     630 7500    1 timeout 900     23   14000    0 false(unreach-call) 86    220 820    1 false(unreach-call) .031 7.7 .12 1 out of memory 470   15000 2500 0 timeout 960   4600 4800 0 timeout 960   6700 7300 0 unknown 890    1200 7100   0 false(unreach-call) 24    530 230   1 timeout 900     1100 7800    0 timeout 900     1100 7200    0 timeout 900     1100 7000    0 error (1) 890     1300   7400    0 unknown .16  9.4 1.6  0 out of memory 550   15000 3300 0 error 88   1900 700 0 out of memory 530   15000 3400 0
floats-cdfpl/newton_3_7_false-unreach-call.i false(unreach-call) 260     400 2600    1 timeout 900     25   13000    0 false(unreach-call) 48    210 450    1 false(unreach-call) 460     4500   3500    1 out of memory 510   15000 3800 0 false(unreach-call) 620   2100 3400 1 false(unreach-call) 42   530 280 1 unknown 890    1100 8400   0 false(unreach-call) 72    540 540   1 timeout 900     1100 8500    0 timeout 900     1100 6700    0 timeout 900     1100 7700    0 error (1) 890     1300   8500    0 unknown .14  9.4 1.7  0 out of memory 480   15000 3400 0 error 77   2000 590 0 out of memory 480   15000 3400 0
floats-cdfpl/newton_3_8_false-unreach-call.i false(unreach-call) 89     210 930    1 timeout 900     25   11000    0 false(unreach-call) 41    220 490    1 false(unreach-call) 200     4500   1500    1 false(unreach-call) 140   3700 820 1 false(unreach-call) 660   2800 3600 1 false(unreach-call) 17   540 140 1 unknown 890    1100 11000   0 false(unreach-call) 56    530 560   1 timeout 900     1100 8700    0 timeout 900     1100 8500    0 timeout 900     1100 7000    0 error (1) 890     1400   9900    0 unknown .14  9.3 1.9  0 false(unreach-call) 50   1400 480 1 error 74   2000 520 0 false(unreach-call) 48   1400 450 1
floats-cdfpl/sine_1_false-unreach-call.i false(unreach-call) 1.9   37 25    1 unknown .072 8.3 .45 0 false(unreach-call) 1.2  33 14    1 false(unreach-call) 65     250   700    1 false(unreach-call) 15   720 170 1 false(unreach-call) 41   760 250 1 false(unreach-call) 11   280 80 1 false(unreach-call) 180    240 1900   1 false(unreach-call) 4.9  120 53   1 false(unreach-call) 170     240 1600    1 false(unreach-call) 180     240 1600    1 false(unreach-call) 180     240 1900    1 false(unreach-call) 140     300   1100    1 unknown .14  9.3 1.5  0 false(unreach-call) 22   890 210 1 error 31   570 280 0 false(unreach-call) 24   880 210 1
floats-cdfpl/sine_2_false-unreach-call.i false(unreach-call) 1.4   34 16    1 unknown .047 8.1 .53 0 false(unreach-call) 1.3  34 18    1 false(unreach-call) 110     240   1100    1 false(unreach-call) 84   2400 700 1 false(unreach-call) 83   1600 460 1 false(unreach-call) 11   290 94 1 false(unreach-call) 89    200 890   1 false(unreach-call) 16    130 170   1 false(unreach-call) 92     190 710    1 false(unreach-call) 89     190 910    1 false(unreach-call) 90     190 920    1 false(unreach-call) 62     280   540    1 unknown .17  9.4 1.8  0 out of memory 440   15000 4000 0 error 31   560 280 0 out of memory 440   15000 3500 0
floats-cdfpl/sine_3_false-unreach-call.i false(unreach-call) 2.5   37 29    1 unknown .048 8.3 .48 0 false(unreach-call) 1.3  32 13    1 false(unreach-call) 82     240   690    1 false(unreach-call) 360   9600 3100 1 false(unreach-call) 74   1300 450 1 false(unreach-call) 12   310 94 1 false(unreach-call) 65    180 570   1 false(unreach-call) 10    130 95   1 false(unreach-call) 62     180 510    1 false(unreach-call) 57     180 740    1 false(unreach-call) 59     180 530    1 false(unreach-call) 51     280   380    1 unknown .17  9.2 1.6  0 false(unreach-call) 86   3400 790 1 error 31   580 230 0 false(unreach-call) 84   3400 940 1
floats-cdfpl/square_1_false-unreach-call.i false(unreach-call) .87  33 11    1 unknown .049 8.0 .59 0 false(unreach-call) .95 32 11    1 false(unreach-call) 56     93   730    1 false(unreach-call) 140   1500 1100 1 false(unreach-call) 68   780 370 1 false(unreach-call) 95   740 770 1 false(unreach-call) 590    200 4100   1 false(unreach-call) 7.2  120 72   1 false(unreach-call) 540     200 5600    1 false(unreach-call) 540     200 5700    1 false(unreach-call) 570     200 4100    1 false(unreach-call) 83     150   780    1 unknown .15  9.3 1.5  0 false(unreach-call) 38   980 310 1 error 30   330 210 0 false(unreach-call) 37   970 290 1
floats-cdfpl/square_2_false-unreach-call.i false(unreach-call) 2.0   34 25    1 unknown .046 7.9 .61 0 false(unreach-call) .85 32 8.7  1 false(unreach-call) 70     100   840    1 false(unreach-call) 51   1100 430 1 false(unreach-call) 63   930 340 1 false(unreach-call) 61   820 620 1 unknown 890    260 7400   0 false(unreach-call) 6.3  120 76   1 timeout 900     350 8000    0 timeout 900     250 6900    0 timeout 900     350 10000    0 false(unreach-call) 130     170   1200    1 unknown .14  9.3 1.6  0 false(unreach-call) 77   1800 530 1 error 29   320 290 0 false(unreach-call) 78   1800 660 1
floats-cdfpl/square_3_false-unreach-call.i false(unreach-call) 2.3   35 33    1 unknown .047 8.1 .56 0 false(unreach-call) 1.5  34 21    1 false(unreach-call) 140     100   1700    1 false(unreach-call) 93   2200 800 1 false(unreach-call) 260   3600 1500 1 false(unreach-call) 140   3400 970 1 unknown 890    350 6300   0 false(unreach-call) 5.7  120 81   1 timeout 900     350 7000    0 timeout 900     350 7800    0 timeout 900     350 7200    0 false(unreach-call) 200     170   2400    1 unknown .15  9.4 1.9  0 false(unreach-call) 110   2900 800 1 error 29   320 220 0 false(unreach-call) 110   2900 810 1
floats-cdfpl/newton_1_1_true-unreach-call.i true 210     130 1600    2 timeout 900     25   10000    0 true 18    66 160    2 true .026 7.7 .13 2 out of memory 670   15000 4000 0 timeout 900   11000 4800 0 timeout 900   6300 6100 0 unknown 890    410 9600   0 true 39    200 370   2 timeout 900     450 7200    0 timeout 900     450 7800    0 timeout 900     450 7600    0 error (1) 890     570   6700    0 unknown .16  9.4 1.8  0 out of memory 490   15000 3800 0 error 82   1100 630 0 out of memory 500   15000 3300 0
floats-cdfpl/newton_1_2_true-unreach-call.i true 46     84 400    2 timeout 900     25   11000    0 true 15    71 150    2 true .015 7.9 .18 2 out of memory 610   15000 3700 0 timeout 900   9300 4500 0 timeout 900   5400 6700 0 unknown 890    400 9900   0 true 45    210 480   2 timeout 900     460 6900    0 timeout 900     460 6700    0 timeout 900     420 3800    0 error (1) 890     570   7900    0 unknown .18  9.4 1.6  0 out of memory 480   15000 3300 0 error 80   1100 600 0 out of memory 490   15000 3200 0
floats-cdfpl/newton_1_3_true-unreach-call.i true 180     140 1600    2 timeout 900     23   11000    0 true 20    78 280    2 true .020 7.9 .14 2 out of memory 690   15000 4600 0 timeout 900   12000 4700 0 timeout 900   6200 6300 0 unknown 890    470 6500   0 true 47    200 530   2 timeout 900     460 6800    0 timeout 900     460 6700    0 timeout 900     460 8300    0 error (1) 890     580   6800    0 unknown .15  9.5 1.4  0 out of memory 460   15000 3100 0 error 78   1000 600 0 out of memory 460   15000 3100 0
floats-cdfpl/newton_2_1_true-unreach-call.i true 140     220 1100    2 timeout 900     25   12000    0 true 47    130 400    2 true .032 7.9 .12 2 out of memory 590   15000 4200 0 timeout 910   12000 4100 0 timeout 900   5600 5600 0 unknown 890    690 11000   0 true 89    390 730   2 timeout 900     740 7900    0 timeout 900     740 5800    0 timeout 900     760 9800    0 error (1) 890     980   6600    0 unknown .15  9.4 1.9  0 out of memory 470   15000 4100 0 error 77   1400 600 0 out of memory 490   15000 3600 0
floats-cdfpl/newton_2_2_true-unreach-call.i true 110     210 890    2 timeout 900     25   12000    0 true 45    130 460    2 true .036 7.6 .11 2 out of memory 620   15000 4200 0 timeout 910   12000 4000 0 timeout 900   6600 6000 0 unknown 890    770 8200   0 true 150    440 1500   2 timeout 900     770 6500    0 timeout 900     770 6900    0 timeout 900     770 7400    0 error (1) 890     970   6900    0 unknown .14  9.3 1.8  0 out of memory 440   15000 2600 0 error 66   1500 500 0 out of memory 450   15000 3300 0
floats-cdfpl/newton_2_3_true-unreach-call.i true 210     290 1800    2 timeout 900     25   12000    0 true 52    130 530    2 true .043 7.8 .14 2 out of memory 580   15000 4000 0 timeout 910   12000 5100 0 timeout 900   7000 6000 0 unknown 890    760 8900   0 true 140    420 960   2 timeout 900     760 8200    0 timeout 900     750 7200    0 timeout 900     760 8100    0 error (1) 890     960   8400    0 unknown .15  9.4 1.7  0 out of memory 480   15000 3100 0 error 72   1500 550 0 out of memory 470   15000 3500 0
floats-cdfpl/newton_2_4_true-unreach-call.i true 410     450 4900    2 timeout 900     23   13000    0 true 51    130 530    2 true .036 7.6 .13 2 out of memory 550   15000 3900 0 timeout 900   12000 4100 0 timeout 900   6000 6500 0 unknown 890    690 9400   0 true 130    410 1000   2 timeout 900     740 7000    0 timeout 900     740 7500    0 timeout 900     740 10000    0 error (1) 890     960   6300    0 unknown .17  9.4 1.9  0 out of memory 530   15000 3600 0 error 67   1500 550 0 out of memory 530   15000 3400 0
floats-cdfpl/newton_2_5_true-unreach-call.i true 280     370 2000    2 timeout 900     25   13000    0 true 77    130 730    2 true .021 7.7 .17 2 out of memory 580   15000 2800 0 timeout 900   11000 3500 0 timeout 900   5700 5900 0 unknown 890    760 8200   0 true 250    430 2000   2 timeout 900     760 8000    0 timeout 900     760 7900    0 timeout 900     760 6800    0 error (1) 890     980   7000    0 unknown .18  9.3 1.8  0 out of memory 500   15000 3600 0 error 73   1500 650 0 out of memory 500   15000 3200 0
floats-cdfpl/newton_3_1_true-unreach-call.i true 400     500 3200    2 timeout 900     25   13000    0 true 110    190 1100    2 true .021 7.7 .16 2 out of memory 650   15000 4000 0 timeout 910   12000 4400 0 timeout 900   6600 7100 0 unknown 890    1000 11000   0 true 390    680 3000   2 timeout 900     1100 7500    0 timeout 900     1100 7000    0 timeout 900     1100 7500    0 error (1) 890     1300   7000    0 unknown .16  9.6 1.8  0 out of memory 440   15000 3000 0 error 77   2000 600 0 out of memory 440   15000 3100 0
floats-cdfpl/newton_3_2_true-unreach-call.i true 360     500 2800    2 timeout 900     25   11000    0 true 150    220 1300    2 true .025 7.5 .13 2 out of memory 570   15000 3700 0 timeout 910   13000 3800 0 timeout 900   7100 6100 0 unknown 890    1000 8800   0 true 370    660 2700   2 timeout 900     1100 8300    0 timeout 900     1100 7400    0 timeout 900     990 2500    0 error (1) 890     1300   6600    0 unknown .18  9.4 2.0  0 out of memory 470   15000 2900 0 error 67   1800 610 0 out of memory 470   15000 3000 0
floats-cdfpl/newton_3_3_true-unreach-call.i true 510     580 4800    2 timeout 900     25   12000    0 true 240    210 2400    2 true .024 7.6 .14 2 out of memory 540   15000 3800 0 timeout 910   12000 4200 0 timeout 900   6800 7300 0 unknown 890    970 9700   0 true 350    660 2900   2 timeout 900     1000 6600    0 timeout 900     1000 7300    0 timeout 900     1000 7700    0 error (1) 890     1300   9500    0 unknown .20  22   2.4  0 out of memory 480   15000 3000 0 error 79   2000 630 0 out of memory 450   15000 3000 0
floats-cdfpl/newton_3_4_true-unreach-call.i true 620     640 5100    2 timeout 900     25   12000    0 true 100    210 830    2 true .041 7.6 .13 2 out of memory 590   15000 4100 0 timeout 910   13000 5600 0 timeout 900   6100 7000 0 unknown 890    1100 7500   0 true 360    660 2500   2 timeout 900     940 7500    0 timeout 900     940 8800    0 timeout 900     950 7300    0 error (1) 890     1300   9800    0 unknown .17  9.3 1.8  0 out of memory 450   15000 4300 0 error 76   1900 620 0 out of memory 450   15000 3100 0
floats-cdfpl/newton_3_5_true-unreach-call.i true 430     500 5000    2 timeout 900     25   12000    0 true 120    220 1200    2 true .029 7.7 .12 2 out of memory 620   15000 3900 0 timeout 910   11000 4800 0 timeout 900   7200 6700 0 unknown 890    1100 6900   0 true 310    640 2400   2 timeout 900     1100 7200    0 timeout 900     1100 7000    0 timeout 900     1100 7100    0 error (1) 890     1300   6400    0 unknown .18  9.4 1.7  0 out of memory 470   15000 2900 0 error 80   1900 800 0 out of memory 460   15000 3100 0
floats-cdfpl/sine_4_true-unreach-call.i true 500     110 5700    2 unknown .048 8.2 .46 0 true 67    55 810    2 true .026 8.0 .13 2 out of memory 460   15000 2900 0 timeout 900   13000 5100 0 timeout 900   7400 6200 0 unknown 890    310 7700   0 true 290    180 2200   2 timeout 900     300 8800    0 timeout 900     300 7600    0 timeout 900     220 2100    0 error (1) 890     470   9200    0 unknown .18  9.4 1.9  0 out of memory 460   15000 2900 0 error 31   580 230 0 out of memory 460   15000 3300 0
floats-cdfpl/sine_5_true-unreach-call.i true 8.3   40 100    2 unknown .049 8.0 .51 0 true 5.4  38 63    2 true .028 7.7 .11 2 out of memory 480   15000 3200 0 timeout 900   13000 4900 0 timeout 900   7500 6500 0 unknown 890    310 8800   0 true 18    130 210   2 timeout 900     300 8300    0 timeout 900     300 9700    0 timeout 900     300 7800    0 error (1) 890     470   7200    0 unknown .17  9.3 1.7  0 out of memory 460   15000 3000 0 error 31   560 250 0 out of memory 450   15000 3300 0
floats-cdfpl/sine_6_true-unreach-call.i true 3.6   40 49    2 unknown .045 7.9 .46 0 true 2.9  33 38    2 true .025 7.9 .13 2 timeout 900   14000 6200 0 timeout 900   14000 4400 0 timeout 900   7000 6600 0 unknown 890    310 9000   0 true 18    130 180   2 timeout 900     310 8400    0 timeout 900     310 6700    0 timeout 900     310 9100    0 error (1) 890     480   5900    0 unknown .18  9.4 1.7  0 out of memory 480   15000 3200 0 error 31   570 270 0 out of memory 480   15000 3100 0
floats-cdfpl/sine_7_true-unreach-call.i true 2.6   38 32    2 unknown .076 7.9 .40 0 true 3.7  34 46    2 true .020 7.8 .20 2 timeout 900   12000 5700 0 timeout 900   14000 5900 0 timeout 900   7200 6600 0 unknown 890    310 6500   0 true 19    130 200   2 timeout 900     300 7200    0 timeout 900     300 6700    0 timeout 900     300 7300    0 error (1) 890     470   8400    0 unknown .22  17   1.6  0 out of memory 460   15000 3500 0 error 31   550 270 0 out of memory 460   15000 3900 0
floats-cdfpl/sine_8_true-unreach-call.i true 15     54 210    2 unknown .081 7.9 .36 0 true 2.7  35 30    2 true 280     250   2400    2 out of memory 520   15000 3600 0 timeout 900   12000 5000 0 timeout 900   6700 7400 0 unknown 890    310 7400   0 true 14    130 150   2 timeout 900     300 7300    0 timeout 900     300 6600    0 timeout 900     300 6900    0 error (1) 890     380   7600    0 unknown .14  9.3 2.0  0 out of memory 460   15000 4300 0 error 31   560 240 0 out of memory 470   15000 3200 0
floats-cdfpl/square_4_true-unreach-call.i true 130     190 1800    2 unknown .082 9.0 .47 0 true 150    62 1600    2 true 200     100   2200    2 out of memory 490   15000 2700 0 timeout 900   11000 4000 0 timeout 900   5500 6800 0 unknown 890    250 6900   0 true 170    160 1300   2 timeout 900     250 6700    0 timeout 900     250 7700    0 timeout 900     350 7600    0 error (1) 890     870   7300    0 unknown .18  9.2 1.7  0 out of memory 460   15000 3000 0 error 29   330 280 0 out of memory 460   15000 2700 0
floats-cdfpl/square_5_true-unreach-call.i true 140     190 1700    2 unknown .073 8.0 .37 0 true 210    59 2700    2 true 260     110   2800    2 out of memory 560   15000 3500 0 timeout 900   11000 4400 0 true 640   6000 4900 2 unknown 890    350 6200   0 true 59    140 510   2 timeout 900     350 6200    0 timeout 900     350 6500    0 timeout 900     350 6400    0 error (1) 890     870   7500    0 unknown .14  9.3 1.7  0 out of memory 460   15000 4100 0 error 30   320 290 0 out of memory 460   15000 3900 0
floats-cdfpl/square_6_true-unreach-call.i true 120     190 1400    2 unknown .050 7.9 .56 0 true 13    48 150    2 true 210     100   2200    2 out of memory 530   15000 3700 0 timeout 900   10000 4100 0 true 880   5600 6300 2 unknown 890    250 7800   0 true 21    120 230   2 timeout 900     350 7500    0 timeout 900     350 7000    0 timeout 900     350 7600    0 error (1) 890     880   6300    0 unknown .17  9.3 1.8  0 out of memory 510   15000 3200 0 error 29   320 250 0 out of memory 510   15000 3300 0
floats-cdfpl/square_7_true-unreach-call.i true 50     120 590    2 unknown .070 8.0 .53 0 true 17    40 230    2 true 180     92   2000    2 out of memory 500   15000 3300 0 true 660   8200 3300 2 true 490   6200 4400 2 unknown 890    260 8200   0 true 43    130 390   2 timeout 900     250 8800    0 timeout 900     250 7200    0 timeout 900     250 6300    0 error (1) 890     870   6300    0 unknown .15  9.4 1.6  0 true 510   11000 3600 2 error 31   340 270 0 true 500   11000 3600 2
floats-cdfpl/square_8_true-unreach-call.i true 1.2   33 14    2 unknown .069 8.3 .45 0 true 2.3  33 31    2 true 56     91   590    2 error 54   800 420 0 true 48   810 300 2 true 97   700 830 2 unknown 890    200 7100   0 true 7.5  120 87   2 timeout 900     200 6200    0 timeout 900     200 6600    0 timeout 900     200 7100    0 true 160     170   1300    2 unknown .14  9.5 1.4  0 true 380   8700 3200 2 error 29   330 300 0 true 400   8700 2400 2
floats-cbmc-regression/float-div1_true-unreach-call.i true .30  35 3.1  2 unknown .057 12   .61 0 true .59 32 6.2  2 true .15  8.2 1.3  2 error 5.4 370 51 0 true 9.1 540 60 2 true 7.5 370 68 2 true 36    370 380   2 true 2.1  110 24   2 timeout 900     3400 12000    0 true 14     130 140    2 true 14     130 180    2 true 6.8   160   67    2 unknown .19  9.5 2.0  0 true 79   680 660 2 error 50   390 420 0 true 79   680 630 2
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true .99  110 10    2 unknown .093 13   .70 0 true .55 35 5.2  2 true .12  8.3 1.6  2 error 5.4 320 41 0 true 23   2400 160 2 true 22   2100 170 2 true 24    2200 210   2 true .36 34 4.4 2 timeout 900     420 14000    0 true .19  28 2.3  2 true .20  28 2.0  2 error (1) .64  45   7.6  0 unknown .22  9.8 2.0  0 true 27   720 300 2 true 18   530 150 2 true 28   720 240 2
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true .10  22 .68 2 true .090 19   1.0  2 true .16 17 1.5  2 true .081 7.6 .27 2 true 2.7 270 25 2 true 2.7 270 23 2 true 2.3 250 18 2 true 3.1  270 30   2 true .14 23 1.7 2 timeout 900     9500 12000    0 true .27  23 .61 2 true .078 23 .79 2 true .88  71   8.9  2 true .16  9.3 1.3  2 true 8.8 300 69 2 error 4.9 320 35 0 true 9.3 320 73 2
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true .70  41 7.7  2 unknown .084 12   .54 0 true 2.4  25 30    2 true .14  8.2 1.1  2 true 3.8 290 32 2 true 25   530 220 2 true 8.8 330 97 2 true 290    320 3400   2 true 3.7  72 53   2 timeout 900     230 9000    0 true 130     93 1700    2 true 140     93 1600    2 true 45     140   550    2 unknown .19  9.5 2.4  0 true 53   450 640 2 error 33   370 370 0 true 55   460 650 2
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true .10  23 .88 2 exception (gremlins) .10  19   .57 0 true .18 17 1.6  2 true .061 7.8 .37 2 true 2.5 270 23 2 true 2.6 270 24 2 true 2.4 230 21 2 true 3.1  270 29   2 true .14 23 1.4 2 timeout 900     9300 12000    0 true .094 23 .70 2 true .10  23 .70 2 true .82  52   8.0  2 true .13  9.3 1.5  2 true 9.2 320 75 2 error 5.0 310 42 0 true 9.4 320 73 2
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true .33  35 2.7  2 unknown .059 12   .54 0 true .46 23 3.3  2 true .15  8.0 1.2  2 error 4.4 300 36 0 true 5.4 320 41 2 true 4.6 290 34 2 true 6.4  300 64   2 true .45 35 4.7 2 out of memory 200     15000 2600    0 true .15  27 1.8  2 true .15  27 1.6  2 true 1.0   82   12    2 unknown .23  9.6 2.3  0 true 17   530 150 2 true 14   480 110 2 true 18   510 160 2
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true .12  22 .86 2 unknown .075 8.4 .52 0 true .16 17 1.6  2 true .091 14   .39 2 true 2.7 270 23 2 true 2.8 280 21 2 true 2.2 240 18 2 true 3.2  250 32   2 true .14 23 1.5 2 timeout 900     7000 12000    0 true .087 23 .82 2 true .075 23 .75 2 true .77  57   12    2 true .15  9.4 1.6  2 true 10   320 92 2 true 13   320 120 2 true 10   320 81 2
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true .12  22 .72 2 timeout 900     25   10000    0 true .16 17 1.4  2 true .042 7.8 .32 2 true 2.5 270 23 2 true 2.7 260 23 2 true 2.2 240 18 2 true 3.0  260 32   2 true .16 23 1.4 2 timeout 900     11000 12000    0 true .078 23 .83 2 true .073 23 .74 2 true .81  51   9.4  2 true .15  9.3 1.4  2 true 10   330 84 2 true 10   330 89 2 true 9.7 310 74 2
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true .20  28 2.0  2 unknown .059 12   .62 0 true .32 21 4.1  2 true .17  44   1.6  2 true 3.5 280 32 2 true 3.4 270 27 2 true 2.8 260 22 2 true 4.3  280 44   2 true .23 27 3.0 2 timeout 900     5500 12000    0 true .12  26 1.3  2 true .13  26 1.4  2 true .92  72   12    2 true .18  9.6 2.3  2 true 11   310 80 2 true 10   310 89 2 true 11   310 86 2
floats-cbmc-regression/float-rounding1_true-unreach-call.i true .23  28 1.6  2 exception (gremlins) .054 15   .57 0 true .39 21 3.2  2 true .12  8.1 1.4  2 error 3.3 270 31 0 error 6.4 440 46 0 unknown 6.3 440 48 0 unknown 8.9  440 81   0 true .43 34 4.5 2 out of memory 520     15000 6800    0 true .28  29 3.7  2 true .28  29 3.5  2 error (1) .058 7.2 .39 0 unknown .14  9.5 1.3  0 unknown 5.3 310 40 0 unknown 5.0 300 42 0 unknown 5.0 310 39 0
floats-cbmc-regression/float-to-double1_true-unreach-call.i true .25  30 1.9  2 unknown .086 12   .50 0 true .42 21 3.1  2 true .44  8.3 5.8  2 true 3.5 280 32 2 true 5.6 320 45 2 true 4.7 300 38 2 true 29    320 390   2 true .56 38 6.4 2 timeout 900     1300 11000    0 true 11     57 140    2 true 11     55 140    2 true 3.9   87   44    2 unknown .18  9.6 2.4  0 true 100   420 1100 2 true 19   300 210 2 true 110   470 1200 2
floats-cbmc-regression/float-to-double2_true-unreach-call.i true .10  22 .71 2 timeout 900     25   13000    0 true .18 17 1.4  2 true .066 7.8 .47 2 true 2.5 270 25 2 true 2.6 290 20 2 true 2.1 240 20 2 true 3.0  250 27   2 true .14 23 1.4 2 timeout 900     8800 13000    0 true .099 23 .88 2 true .077 23 .89 2 true .80  58   9.3  2 true .16  9.2 1.3  2 true 9.9 330 88 2 true 11   360 79 2 true 9.7 320 82 2
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true .081 22 1.0  2 timeout 900     25   12000    0 true .15 17 1.5  2 true .067 7.8 .37 2 true 2.7 270 24 2 true 2.8 260 27 2 true 2.4 250 18 2 true 3.1  260 33   2 true .19 24 2.3 2 out of memory 64     15000 790    0 true .28  23 .66 2 true .077 23 .89 2 true .81  53   8.2  2 true .13  9.4 1.4  2 unknown 5.3 320 41 0 unknown 4.7 300 34 0 unknown 4.7 310 35 0
floats-cbmc-regression/float11_true-unreach-call.i true .12  22 .80 2 unknown .061 8.5 .38 0 true .16 17 1.6  2 true .061 7.9 .42 2 true 2.5 260 21 2 true 2.7 260 22 2 true 2.4 250 21 2 true 3.4  260 33   2 true .16 24 2.3 2 timeout 900     3000 13000    0 true .10  24 1.2  2 true .088 24 1.1  2 true .80  52   7.8  2 true .14  9.4 1.1  2 true 9.9 320 77 2 true 11   340 80 2 true 11   340 87 2
floats-cbmc-regression/float12_true-unreach-call.i true .089 22 .88 2 true .13  20   .97 2 true .20 17 1.8  2 true .20  8.5 2.3  2 true 2.5 260 25 2 true 3.1 270 23 2 true 3.0 290 23 2 true 7.6  280 86   2 true .28 26 3.4 2 timeout 900     5400 11000    0 true 1.9   36 22    2 true 1.9   36 26    2 true 1.1   74   15    2 unknown .17  9.3 1.5  0 true 16   320 160 2 true 19   320 270 2 true 16   310 150 2
floats-cbmc-regression/float13_true-unreach-call.i true .14  23 1.1  2 unknown .070 8.8 .44 0 true .17 17 1.6  2 true .15  7.9 1.5  2 true 2.7 270 24 2 true 2.8 270 22 2 true 2.3 240 21 2 true 3.0  260 27   2 true .14 23 1.5 2 timeout 900     5100 15000    0 true .078 23 .82 2 true .087 23 .78 2 true .82  55   10    2 true .15  9.5 1.6  2 true 10   330 85 2 true 12   350 97 2 true 10   320 89 2
floats-cbmc-regression/float14_true-unreach-call.i true .21  28 1.4  2 unknown .055 12   .61 0 true .38 21 3.2  2 true .12  8.4 1.5  2 true 3.7 290 33 2 true 3.4 280 25 2 true 2.7 260 24 2 true 4.3  270 42   2 true .23 27 2.6 2 timeout 900     4700 11000    0 true .12  26 1.3  2 true .13  26 1.2  2 true .87  67   9.8  2 unknown .17  9.6 2.0  0 true 11   320 100 2 true 10   300 79 2 true 11   310 82 2
floats-cbmc-regression/float18_true-unreach-call.i timeout 900     1800 9400    0 exception (gremlins) .16  25   1.0  0 true .97 21 12    2 true .066 8.2 .55 2 true 4.0 290 31 2 true 3.7 270 29 2 true 2.8 260 27 2 true 18    260 230   2 true .52 39 5.4 2 timeout 900     3700 13000    0 true .29  35 3.7  2 unknown .16  26 1.2  0 true .80  61   10    2 true .20  9.4 2.4  2 unknown 4.7 300 39 0 unknown 5.2 310 42 0 unknown 5.1 300 42 0
floats-cbmc-regression/float19_true-unreach-call.i true .19  28 1.8  2 false(unreach-call) .069 22   .68 -16 true .32 21 4.2  2 true .17  8.3 2.3  2 error 4.1 310 33 0 true 4.7 330 34 2 true 4.2 300 36 2 true 7.3  330 69   2 true .35 26 3.9 2 timeout 900     6200 14000    0 true .85  30 11    2 true 3.5   30 6.9  2 true 1.1   68   13    2 unknown .17  9.5 2.2  0 true 12   340 100 2 true 11   300 87 2 true 11   310 94 2
floats-cbmc-regression/float1_true-unreach-call.i true .097 22 .73 2 unknown .081 9.1 .43 0 true .19 17 1.3  2 true .066 7.8 .45 2 true 2.6 260 22 2 true 2.8 270 23 2 true 2.3 250 22 2 true 3.0  230 31   2 true .13 23 1.7 2 timeout 900     7800 11000    0 true .11  23 .66 2 true .092 23 .75 2 true .80  56   9.3  2 true .16  9.3 1.4  2 true 9.3 310 77 2 error 4.9 300 39 0 true 9.6 320 70 2
floats-cbmc-regression/float20_true-unreach-call.i true .11  25 1.3  2 unknown .083 8.1 .37 0 true .20 22 1.8  2 true .33  47   4.1  2 true 2.8 270 23 2 true 2.8 270 21 2 true 2.3 250 21 2 true 22    260 230   2 true .60 46 7.8 2 timeout 900     3200 8400    0 true 9.6   91 110    2 true 9.9   91 110    2 true 2.2   110   24    2 unknown .18  9.4 1.8  0 true 23   390 240 2 error 22   330 270 0 true 23   390 230 2
floats-cbmc-regression/float21_true-unreach-call.i true .30  30 2.2  2 unknown .056 12   .61 0 true .46 24 4.6  2 true .15  8.2 1.1  2 error 4.5 310 39 0 true 8.6 500 64 2 true 4.7 300 41 2 true 30    310 300   2 true .53 39 5.4 2 timeout 900     1400 13000    0 true 12     64 150    2 true 12     64 140    2 true 56     270   680    2 unknown .20  9.5 1.9  0 true 61   610 680 2 true 51   580 640 2 true 68   620 800 2
floats-cbmc-regression/float22_true-unreach-call.i true .097 22 .82 2 unknown .049 8.3 .55 0 true .18 17 1.8  2 true .060 7.9 .53 2 error 3.0 280 26 0 false(unreach-call) 5.0 320 37 -16 unknown 5.2 330 43 0 unknown 17    51 200   0 true .45 36 5.1 2 unknown .078 24 .81 0 unknown .10  23 .67 0 unknown .072 24 .84 0 out of memory 73     15000   520    0 true .16  9.3 1.3  2 unknown 12   360 96 0 unknown 12   350 93 0 unknown 11   320 91 0
floats-cbmc-regression/float2_true-unreach-call.i true .080 22 .89 2 unknown .067 8.8 .45 0 true .16 17 1.5  2 true .16  43   .92 2 true 2.6 270 23 2 true 2.9 290 23 2 true 2.3 240 19 2 true 2.9  220 27   2 true .15 23 1.4 2 timeout 900     7600 12000    0 true .11  23 .61 2 true .082 23 .82 2 true .81  57   8.2  2 true .13  9.5 1.6  2 true 9.8 320 80 2 true 11   330 90 2 true 10   310 74 2
floats-cbmc-regression/float3_true-unreach-call.i true .098 24 .95 2 true 1.2   25   16    2 true .18 19 2.1  2 true .078 7.6 .56 2 true 2.7 270 22 2 true 2.7 260 21 2 true 2.3 250 19 2 true 7.7  300 80   2 true .67 50 7.9 2 timeout 900     7300 10000    0 true 2.2   47 29    2 true 2.1   47 26    2 true 1.1   85   14    2 true .17  9.7 1.6  2 true 16   340 150 2 true 16   340 140 2 true 18   330 170 2
floats-cbmc-regression/float4_true-unreach-call.i true 8.6   51 140    2 unknown .055 12   .72 0 true 15    40 190    2 true .11  8.2 1.3  2 true 3.8 280 35 2 true 58   790 470 2 true 17   580 200 2 true 320    590 3300   2 true 14    110 160   2 timeout 900     230 9500    0 true 460     94 1100    2 true 130     94 1500    2 true 52     150   600    2 unknown .22  9.6 2.0  0 true 88   530 1000 2 error 77   430 960 0 true 89   510 1100 2
floats-cbmc-regression/float5_true-unreach-call.i true .093 23 .87 2 exception (gremlins) .10  21   .76 0 true .20 19 1.7  2 true .37  9.2 4.9  2 true 2.5 270 24 2 true 2.8 270 23 2 true 2.2 240 20 2 true 16    250 190   2 true .33 26 3.9 2 timeout 900     2300 11000    0 true 6.4   45 81    2 true 6.4   45 78    2 true 1.2   63   14    2 unknown .16  9.3 1.7  0 true 28   340 290 2 true 48   310 600 2 true 28   310 320 2
floats-cbmc-regression/float6_true-unreach-call.i true .14  23 .93 2 unknown .051 10   .54 0 true .18 18 1.7  2 true .074 7.8 .46 2 true 2.8 270 25 2 true 2.8 260 24 2 true 2.3 240 20 2 true 3.6  260 34   2 true .24 24 3.0 2 out of memory 510     15000 980    0 true .13  24 1.0  2 true .13  24 1.0  2 true .83  60   11    2 unknown .16  9.3 1.6  0 true 11   320 83 2 true 17   450 160 2 true 10   330 76 2
floats-cbmc-regression/float7_true-unreach-call.i true .079 22 .79 2 true .10  19   .82 2 true .19 17 1.5  2 true .054 7.7 .30 2 false(unreach-call) 2.8 280 24 -16 true 2.8 300 23 2 true 2.3 250 21 2 true 3.0  260 33   2 true .20 23 2.1 2 out of memory 45     15000 600    0 true .11  23 .68 2 true .10  23 .75 2 true .80  61   12    2 true .16  9.4 1.4  2 unknown 5.1 320 35 0 unknown 5.6 330 47 0 unknown 4.8 310 35 0
floats-cbmc-regression/float8_true-unreach-call.i true .54  29 5.5  2 true .12  23   .84 2 true .92 22 10    2 true .14  8.1 1.1  2 true 3.4 290 30 2 true 7.3 340 51 2 true 6.3 320 61 2 true 7.9  340 75   2 true 1.1  43 13   2 out of memory 64     15000 870    0 true .13  26 1.4  2 true .13  26 1.4  2 true .82  60   9.3  2 unknown .23  9.7 2.4  0 true 10   300 97 2 true 9.3 300 70 2 true 10   300 86 2
floats-cbmc-regression/float_lib1_true-unreach-call.i true .40  32 4.4  2 unknown .092 12   .45 0 true .39 23 4.0  2 true .12  8.0 1.2  2 true 4.6 300 40 2 true 3.5 270 28 2 true 2.8 260 24 2 true 4.5  260 48   2 true .28 28 3.3 2 timeout 900     1000 12000    0 true .16  26 1.7  2 true .14  26 1.9  2 true .91  69   10    2 unknown .17  9.5 2.1  0 error 10   340 83 0 true 16   510 150 2 error 9.2 310 77 0
floats-cbmc-regression/float_lib2_true-unreach-call.i true .23  29 1.9  2 unknown .085 12   .57 0 true .43 22 3.5  2 true .067 8.3 .56 2 true 4.5 300 32 2 true 3.6 270 28 2 true 2.8 260 23 2 true 4.4  280 48   2 true .25 27 2.9 2 timeout 900     1300 13000    0 true .15  26 1.4  2 true .14  26 1.5  2 true 2.4   250   24    2 unknown .17  9.6 1.9  0 true 13   450 110 2 true 20   520 200 2 true 13   450 99 2
float-benchs/cast_float_ptr_false-unreach-call.c false(unreach-call) .13  23 1.1  1 timeout 900     25   11000    0 false(unreach-call) .15 17 .99 1 false(unreach-call) .10  7.6 1.3  1 assertion 1.5 130 14 0 exception 3.0 270 23 0 false(unreach-call) 2.7 250 23 1 false(unreach-call) .39 49 5.0 1 false(unreach-call) .34 32 4.1 1 false(unreach-call) .092 23 1.1  1 false(unreach-call) .086 23 .94 1 false(unreach-call) .11  23 1.0  1 error (1) 890     3000   7500    0 unknown .17  9.4 1.5  0 unknown 4.9 310 38 0 unknown 4.7 300 34 0 unknown 5.5 320 48 0
float-benchs/cast_union_loose_false-unreach-call.c false(unreach-call) .15  25 .93 1 timeout 900     25   12000    0 false(unreach-call) .15 18 1.0  1 false(unreach-call) .13  7.7 1.2  1 true 2.9 300 31 -32 false(unreach-call) 4.2 310 33 1 false(unreach-call) 2.6 250 23 1 false(unreach-call) .49 49 6.0 1 false(unreach-call) .56 43 6.0 1 false(unreach-call) .21  27 2.4  1 false(unreach-call) .18  27 2.0  1 false(unreach-call) .18  27 2.1  1 false(unreach-call) 3.9   120   46    1 false(unreach-call) .17  9.3 1.7  1 unknown 5.1 300 40 0 unknown 4.8 300 35 0 unknown 5.3 300 44 0
float-benchs/cast_union_tight_false-unreach-call.c false(unreach-call) .12  24 1.2  1 false(unreach-call) .11  20   .52 1 false(unreach-call) .14 20 .98 1 false(unreach-call) .11  7.8 1.2  1 false(unreach-call) 3.2 310 32 1 false(unreach-call) 4.1 320 28 1 false(unreach-call) 2.6 250 24 1 false(unreach-call) 1.1  49 14   1 false(unreach-call) .61 45 6.9 1 false(unreach-call) .89  37 10    1 false(unreach-call) .87  37 13    1 false(unreach-call) .90  37 10    1 false(unreach-call) 4.7   140   50    1 unknown .16  9.6 1.6  0 unknown 4.8 300 35 0 unknown 5.1 300 42 0 unknown 5.5 310 44 0
float-benchs/float_int_inv_square_false-unreach-call.c false(unreach-call) .18  26 1.2  1 exception (gremlins) .12  20   .81 0 false(unreach-call) .14 19 1.1  1 false(unreach-call) .56  11   6.0  1 false(unreach-call) 3.2 290 32 1 false(unreach-call) 3.8 310 30 1 false(unreach-call) 2.6 270 24 1 false(unreach-call) 17    69 220   1 false(unreach-call) .40 35 4.8 1 false(unreach-call) .42  33 4.4  1 false(unreach-call) .44  33 5.0  1 false(unreach-call) .43  33 5.1  1 false(unreach-call) 1.3   67   17    1 false(unreach-call) .19  12   2.0  1 false(unreach-call) 10   320 87 1 false(unreach-call) 16   350 140 1 false(unreach-call) 11   330 99 1
float-benchs/inv_square_false-unreach-call.c false(unreach-call) .17  26 1.0  1 timeout 900     25   12000    0 false(unreach-call) .13 19 1.2  1 false(unreach-call) .42  9.3 5.7  1 false(unreach-call) 3.0 300 27 1 false(unreach-call) 4.0 310 31 1 false(unreach-call) 2.5 250 24 1 false(unreach-call) .48 41 5.1 1 false(unreach-call) .35 31 3.4 1 false(unreach-call) .19  23 1.7  1 false(unreach-call) .19  23 1.7  1 false(unreach-call) .15  23 2.1  1 false(unreach-call) .87  61   11    1 unknown .17  9.4 1.6  0 false(unreach-call) 9.4 320 86 1 false(unreach-call) 12   320 140 1 false(unreach-call) 9.9 310 78 1
float-benchs/nan_double_false-unreach-call.c false(unreach-call) .096 22 1.2  1 exception (gremlins) .098 19   .78 0 false(unreach-call) .14 17 .91 1 false(unreach-call) .053 7.7 .32 1 true 2.6 270 21 -32 false(unreach-call) 3.4 290 29 1 false(unreach-call) 2.5 250 23 1 false(unreach-call) .37 48 3.9 1 false(unreach-call) .19 25 2.2 1 false(unreach-call) .10  23 .72 1 false(unreach-call) .11  23 .74 1 false(unreach-call) .099 23 .76 1 false(unreach-call) .80  49   10    1 unknown .16  9.3 1.6  0 false(unreach-call) 6.2 340 45 1 false(unreach-call) 9.1 320 68 1 false(unreach-call) 5.7 330 49 1
float-benchs/nan_float_false-unreach-call.c false(unreach-call) .11  22 .92 1 exception (gremlins) .14  22   .53 0 false(unreach-call) .12 17 .93 1 false(unreach-call) .046 7.6 .48 1 true 2.6 270 23 -32 false(unreach-call) 3.5 290 28 1 false(unreach-call) 2.4 260 21 1 false(unreach-call) .37 48 4.4 1 false(unreach-call) .20 25 2.3 1 false(unreach-call) .098 23 .77 1 false(unreach-call) .075 23 .80 1 false(unreach-call) .079 23 .74 1 false(unreach-call) .78  59   11    1 unknown .16  9.2 1.5  0 false(unreach-call) 5.8 320 45 1 false(unreach-call) 8.8 320 76 1 false(unreach-call) 5.4 310 41 1
float-benchs/sin_interpolated_index_false-unreach-call.c false(unreach-call) 6.5   220 71    1 timeout 900     27   13000    0 false(unreach-call) 2.8  240 30    1 false(unreach-call) .022 8.1 .20 1 false(unreach-call) 3.6 300 30 1 false(unreach-call) 190   550 2500 1 false(unreach-call) 3.7 320 33 1 false(unreach-call) 130    440 1300   1 false(unreach-call) 8.4  320 94   1 false(unreach-call) 260     880 2100    1 false(unreach-call) 240     890 2600    1 false(unreach-call) 250     880 2300    1 false(unreach-call) 160     580   1300    1 unknown .16  9.3 1.9  0 out of memory 220   15000 2300 0 error 5.3 320 40 0 out of memory 210   15000 2300 0
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) .99  39 8.5  1 timeout 900     25   12000    0 false(unreach-call) .50 41 6.7  1 false(unreach-call) .12  7.9 1.4  1 false(unreach-call) 88   2200 1000 1 false(unreach-call) 27   920 170 1 false(unreach-call) 14   380 110 1 false(unreach-call) 290    340 2600   1 false(unreach-call) 7.9  270 78   1 false(unreach-call) 340     340 2700    1 false(unreach-call) 290     340 2300    1 false(unreach-call) 300     340 2800    1 error (1) .15  24   1.7  0 unknown .18  9.3 1.8  0 error 8.1 300 71 0 error 8.8 320 77 0 error 8.9 340 64 0
float-benchs/Muller_Kahan_true-unreach-call.c timeout 900     450 10000    0 exception (gremlins) .071 20   .83 0 true 1.1  17 12    2 out of memory 15     15000   190    0 out of memory 410   15000 5100 0 true 4.3 340 31 2 true 3.1 260 26 2 unknown 890    1200 11000   0 true .18 23 1.8 2 timeout 900     2100 13000    0 true .93  60 13    2 timeout 900     870 3100    0 out of memory 33     15000   390    0 true .13  9.2 1.5  2 timeout 900   7100 8800 0 error 300   2400 2500 0 out of memory 780   15000 7600 0
float-benchs/Rump_double_true-unreach-call.c true .13  25 1.6  2 exception (gremlins) .12  22   1.1  0 true .18 17 1.5  2 true .065 7.9 .41 2 true 2.6 270 26 2 true 2.8 270 24 2 true 2.3 240 19 2 true 3.1  260 32   2 true .15 23 1.4 2 timeout 900     3300 11000    0 true .092 23 .77 2 true .11  23 .77 2 true 230     540   2700    2 true .16  9.2 1.6  2 true 19   800 170 2 error 24   1500 180 0 true 21   800 190 2
float-benchs/Rump_float_true-unreach-call.c true .13  23 1.0  2 exception (gremlins) .16  21   .83 0 true .19 17 1.7  2 true .10  7.9 .41 2 true 2.7 270 27 2 true 2.7 270 24 2 true 2.2 240 19 2 true 3.0  240 29   2 true .13 24 1.4 2 timeout 900     3800 13000    0 true .072 23 .95 2 true .075 23 .79 2 true 22     200   230    2 true .13  9.4 1.5  2 true 12   380 120 2 error 21   540 150 0 true 12   370 96 2
float-benchs/addsub_double_exact_true-unreach-call.c true .10  22 .82 2 true .14  21   1.4  2 true .20 17 1.5  2 true .037 7.9 .36 2 true 2.7 260 22 2 true 2.9 270 22 2 true 2.2 240 20 2 true 3.1  260 34   2 true .13 23 1.5 2 timeout 900     9100 14000    0 true .074 23 .82 2 true .081 23 .72 2 true .84  62   9.6  2 true .15  9.4 1.4  2 true 9.8 320 82 2 error 19   320 230 0 true 9.9 310 87 2
float-benchs/addsub_float_exact_true-unreach-call.c true .11  22 .78 2 true .14  21   1.1  2 true .18 17 1.6  2 true .042 7.8 .27 2 true 2.7 270 21 2 true 2.6 260 20 2 true 2.4 240 21 2 true 2.9  250 32   2 true .13 23 1.5 2 timeout 900     9400 11000    0 true .086 23 .82 2 true .085 23 .84 2 true .80  51   9.2  2 true .22  18   2.0  2 true 10   330 83 2 true 9.9 320 85 2 true 11   330 85 2
float-benchs/addsub_float_inexact_true-unreach-call.c true .088 22 1.0  2 false(unreach-call) .074 21   .62 -16 true .18 17 1.4  2 true .041 7.6 .35 2 true 2.6 270 24 2 true 2.7 260 22 2 true 2.3 250 19 2 true 3.2  270 31   2 true .12 23 1.5 2 timeout 900     9500 12000    0 true .095 23 .81 2 true .10  23 .74 2 true .86  60   8.2  2 true .15  9.3 1.4  2 true 9.7 330 76 2 true 11   330 94 2 true 9.2 310 77 2
float-benchs/arctan_Pade_true-unreach-call.c true 140     500 1600    2 timeout 900     25   11000    0 true 100    250 1100    2 true 470     1900   3500    2 error 14   600 120 0 true 25   940 190 2 true 37   940 330 2 unknown 890    1100 7800   0 true 96    1200 610   2 timeout 900     1100 7300    0 timeout 900     1100 7300    0 timeout 900     1100 8500    0 error (1) 890     1700   6900    0 unknown .16  9.4 1.8  0 error 180   2700 1500 0 error 54   810 380 0 error 39   1200 370 0
float-benchs/bary_diverge_true-unreach-call.c timeout 900     390 9600    0 timeout 900     25   12000    0 error (42) 850    1200 7000    0 true 850     510   11000    2 timeout 900   4600 11000 0 timeout 900   5000 8900 0 timeout 900   4700 8600 0 unknown 890    270 10000   0 true 13    3500 140   2 timeout 900     2000 11000    0 timeout 900     3400 8400    0 timeout 900     4300 8600    0 error (1) 890     1900   9800    0 timeout (timeout) 900     42   12000    0 timeout 900   870 9100 0 error 5.0 300 37 0 timeout 900   770 9400 0
float-benchs/cast_float_union_true-unreach-call.c true .13  23 .86 2 true .051 16   .65 2 true .18 17 1.6  2 true .10  7.9 1.1  2 true 2.7 280 24 2 true 3.0 270 26 2 true 2.3 240 20 2 true 3.1  260 30   2 true .16 23 1.4 2 timeout 900     12000 12000    0 true .12  23 .79 2 true .079 23 .97 2 true .84  61   8.9  2 true .14  9.5 1.6  2 error 8.1 300 62 0 error 8.0 300 63 0 error 8.4 310 68 0
float-benchs/cos_polynomial_true-unreach-call.c true 9.4   88 92    2 timeout 900     24   11000    0 true 10    110 100    2 true 850     1300   4800    2 out of memory 500   15000 3500 0 timeout 910   11000 4700 0 timeout 900   5000 6400 0 unknown 890    620 7500   0 true 36    550 300   2 timeout 900     610 8300    0 timeout 900     610 7800    0 timeout 900     610 7400    0 error (1) 890     460   7500    0 unknown .18  9.5 1.7  0 error 670   8900 5400 0 error 150   960 1100 0 error 810   8900 6400 0
float-benchs/divmul_buf_diverge_true-unreach-call.c true .67  32 7.2  2 timeout 900     25   13000    0 error (42) 850    3200 6200    0 true .045 7.9 .15 2 timeout 900   4200 10000 0 timeout 900   3700 8300 0 timeout 900   3600 8500 0 unknown 890    280 9400   0 true 11    2700 120   2 timeout 900     490 11000    0 timeout 900     14000 11000    0 timeout 900     520 11000    0 true 59     2600   650    2 timeout (timeout) 900     3600   9300    0 timeout 900   4200 14000 0 timeout 900   3900 12000 0 timeout 900   5300 12000 0
float-benchs/divmul_diverge_true-unreach-call.c timeout 900     490 9000    0 timeout 900     25   14000    0 error (42) 850    3100 6900    0 true .033 7.6 .15 2 timeout 900   4200 11000 0 timeout 900   5900 8000 0 timeout 900   3700 8100 0 unknown 890    260 9700   0 true 11    3700 120   2 timeout 900     480 12000    0 timeout 900     13000 10000    0 timeout 900     430 8200    0 true 35     2500   340    2 timeout (timeout) 900     3800   8500    0 timeout 900   3500 12000 0 timeout 900   4100 12000 0 timeout 900   3700 14000 0
float-benchs/drift_tenth_true-unreach-call.c true .68  36 8.2  2 exception (gremlins) .081 20   .58 0 true .49 17 4.4  2 true .21  7.8 2.0  2 true 4.0 280 35 2 true 2.8 270 21 2 true 2.3 240 21 2 unknown 890    490 7400   0 true .17 23 1.5 2 timeout 900     6900 11000    0 true .12  23 .76 2 true 180     210 1500    2 true .82  55   9.1  2 true .14  9.3 1.5  2 true 430   630 4000 2 timeout 900   650 8900 0 true 840   900 7900 2
float-benchs/exp_loop_true-unreach-call.c true 35     240 380    2 exception (gremlins) .093 19   .64 0 true 1.8  30 23    2 unknown 8.6   94   100    0 error 4.7 330 41 0 true 630   8900 6000 2 true 730   10000 6300 2 unknown 890    380 7500   0 true 11    3100 110   2 timeout 900     1400 12000    0 true 760     1500 6500    2 timeout 900     790 8000    0 error (1) 890     2000   9200    0 unknown .16  9.3 2.1  0 timeout 900   1600 9400 0 error 190   630 2000 0 timeout 900   1100 12000 0
float-benchs/feedback_diverge_true-unreach-call.c timeout 900     1400 11000    0 timeout 900     23   12000    0 error (42) 850    1100 8800    0 true .028 7.8 .12 2 timeout 900   4200 12000 0 timeout 900   3500 8300 0 timeout 900   3200 7900 0 unknown 890    310 8400   0 true 11    3300 110   2 timeout 900     520 11000    0 timeout 900     13000 11000    0 timeout 900     460 7600    0 error (1) 890     1700   7400    0 timeout (timeout) 900     3600   8200    0 timeout 900   4100 12000 0 timeout 900   3700 13000 0 timeout 900   3700 11000 0
float-benchs/filter1_true-unreach-call.c timeout 900     1100 11000    0 timeout 900     23   12000    0 error (42) 850    1500 7400    0 true 850     310   10000    2 true 3.4 280 28 2 true 28   1300 170 2 true 20   900 150 2 unknown 890    300 7100   0 true 11    3800 130   2 timeout 900     260 8500    0 timeout 900     270 8800    0 timeout 900     270 8000    0 error (1) 890     2700   8800    0 timeout (timeout) 900     3600   12000    0 timeout 900   940 11000 0 error 61   390 570 0 timeout 900   960 9600 0
float-benchs/filter2_alt_true-unreach-call.c timeout 900     440 8600    0 timeout 900     25   13000    0 error (42) 850    180 10000    0 true 850     190   12000    2 error 12   410 130 0 timeout 900   1200 7300 0 timeout 900   1200 6600 0 unknown 890    230 8600   0 true 11    4600 110   2 timeout 900     250 8000    0 timeout 900     270 9100    0 timeout 900     280 10000    0 error (1) 890     3300   8100    0 timeout (timeout) 900     45   12000    0 timeout 900   860 8400 0 error 35   340 450 0 timeout 900   870 9200 0
float-benchs/filter2_iterated_true-unreach-call.c timeout 900     420 8500    0 timeout 900     25   12000    0 error (42) 850    1100 3800    0 out of memory 30     15000   340    0 error 14   560 140 0 segmentation fault 20   1600 150 0 segmentation fault 9.1 740 82 0 unknown 890    6500 7700   0 true 12    3000 150   2 out of memory 540     15000 7000    0 out of memory 260     15000 3600    0 out of memory 870     15000 10000    0 out of memory 40     15000   430    0 timeout (timeout) 900     15000   11000    0 error 39   2200 420 0 error 24   2200 320 0 error 38   2200 420 0
float-benchs/filter2_reinit_true-unreach-call.c timeout 900     340 8900    0 timeout 900     25   13000    0 error (42) 850    490 7500    0 true 850     360   9300    2 timeout 900   3900 11000 0 timeout 900   3200 8400 0 timeout 900   2700 8400 0 unknown 890    250 6900   0 true 14    3800 150   2 timeout 900     240 7200    0 timeout 900     250 9800    0 timeout 900     220 4600    0 error (1) 890     7700   10000    0 timeout (timeout) 900     51   11000    0 timeout 900   2400 6300 0 error 50   410 460 0 timeout 900   2400 6600 0
float-benchs/filter2_set_true-unreach-call.c timeout 900     330 11000    0 timeout 900     25   13000    0 error (42) 850    440 9100    0 true 850     440   10000    2 error 38   820 390 0 timeout 900   4600 8200 0 timeout 900   3900 9500 0 unknown 890    440 7400   0 true 14    4200 140   2 timeout 900     530 8700    0 timeout 900     560 8400    0 timeout 900     560 8700    0 error (1) 890     13000   4000    0 unknown .19  9.5 2.0  0 timeout 900   4500 8900 0 error 31   510 230 0 timeout 900   4500 6500 0
float-benchs/filter2_true-unreach-call.c timeout 900     490 9600    0 timeout 900     25   13000    0 error (42) 850    480 8800    0 true 850     250   12000    2 true 32   1400 270 2 timeout 900   4500 8800 0 timeout 900   4300 9300 0 unknown 890    530 7000   0 true 13    4300 130   2 timeout 900     380 9300    0 timeout 900     400 9400    0 timeout 900     400 8600    0 error (1) 890     6300   8100    0 timeout (timeout) 900     46   11000    0 timeout 900   2800 7800 0 error 30   390 300 0 timeout 900   2700 6800 0
float-benchs/filter_iir_true-unreach-call.c true .43  53 6.2  2 timeout 900     25   12000    0 error (42) 850    750 6800    0 true 850     650   6500    2 true 3.2 280 29 2 true 3.4 280 26 2 true 2.6 250 22 2 unknown 890    780 11000   0 true 14    4200 160   2 timeout 900     420 8100    0 timeout 900     440 7000    0 timeout 900     440 7800    0 out of memory 40     15000   420    0 timeout (timeout) 900     47   11000    0 unknown 4.9 310 39 0 unknown 4.7 300 39 0 unknown 6.2 340 52 0
float-benchs/float_double_true-unreach-call.c true .12  22 .69 2 false(unreach-call) .090 17   .70 -16 true .18 17 1.7  2 true .078 7.8 .46 2 true 2.6 270 25 2 true 2.6 270 20 2 true 2.2 240 21 2 true 3.2  270 28   2 true .16 23 1.3 2 timeout 900     9900 11000    0 true .098 23 .80 2 true .072 23 .77 2 true .83  60   8.9  2 true .13  9.5 1.7  2 true 11   330 87 2 true 10   320 79 2 true 9.8 310 83 2
float-benchs/image_filter_true-unreach-call.c timeout 900     1100 12000    0 timeout 900     27   12000    0 true 830    2800 8000    2 out of memory 18     15000   180    0 timeout 900   4900 10000 0 segmentation fault 11   560 74 0 out of memory 240   15000 2900 0 unknown 890    3100 8300   0 true 11    1300 140   2 timeout 900     2200 11000    0 timeout 900     2300 9500    0 timeout 900     2200 8000    0 out of memory 60     15000   700    0 unknown .24  11   2.3  0 unknown 4.7 290 37 0 unknown 4.8 300 42 0 unknown 5.3 320 40 0
float-benchs/interpolation2_true-unreach-call.c true .56  28 8.2  2 timeout 900     25   14000    0 true .80 26 9.9  2 true .11  7.7 1.1  2 segmentation fault 4.2 350 37 0 segmentation fault 11   390 99 0 segmentation fault 3.6 330 32 0 unknown 710    350 7300   0 true 2.6  85 28   2 timeout 900     270 9400    0 true 610     260 5500    2 true 610     320 7200    2 error (1) 890     1700   3800    0 unknown .16  9.5 1.7  0 timeout 900   550 9100 0 error 69   370 670 0 timeout 900   560 13000 0
float-benchs/interpolation_true-unreach-call.c true .24  27 2.3  2 exception (gremlins) .081 21   .79 0 true .51 23 6.2  2 true .13  8.1 1.0  2 exception 3.7 330 40 0 segmentation fault 8.2 370 65 0 exception 3.5 310 32 0 unknown 140    320 1500   0 true 1.5  63 15   2 timeout 900     1000 9100    0 true 120     180 1300    2 true 150     220 1400    2 error (1) 890     2400   6500    0 unknown .17  9.6 2.0  0 out of memory 340   15000 4500 0 error 52   330 500 0 out of memory 340   15000 3700 0
float-benchs/inv_sqrt_Quake_true-unreach-call.c true .24  28 2.2  2 false(unreach-call) .095 20   .73 -16 true .46 25 5.0  2 true 8.9   48   130    2 false(unreach-call) 4.2 340 44 -16 false(unreach-call) 4.7 330 39 -16 false(unreach-call) 2.8 260 23 -16 false(unreach-call) 320    260 2800   -16 true 1.2  61 14   2 timeout 900     330 11000    0 true 130     100 1200    2 true 130     100 1300    2 error (1) .056 7.3 .47 0 unknown .15  9.4 2.2  0 unknown 5.3 320 40 0 unknown 6.0 340 47 0 unknown 4.8 310 37 0
float-benchs/inv_square_int_true-unreach-call.c true .16  26 1.2  2 exception (gremlins) .089 21   .89 0 true .22 21 1.7  2 true .14  8.8 1.5  2 error 3.0 290 25 0 true 3.8 300 26 2 true 3.5 290 34 2 true 27    310 330   2 true .37 33 4.3 2 timeout 900     2500 6500    0 true 3.2   40 48    2 true 3.2   40 42    2 true 1.5   82   17    2 true .18  10   1.6  2 true 37   360 400 2 true 13   340 120 2 true 41   350 520 2
float-benchs/inv_square_true-unreach-call.c true .14  26 1.2  2 timeout 900     25   12000    0 true .24 20 2.0  2 true .72  9.1 9.3  2 error 3.0 290 29 0 true 3.6 300 27 2 true 3.2 280 29 2 true 5.3  290 58   2 true .34 29 3.6 2 timeout 900     7500 12000    0 true .72  25 9.7  2 true .72  25 11    2 true .95  67   11    2 unknown .17  9.4 1.8  0 true 69   340 820 2 true 15   320 150 2 true 91   370 930 2
float-benchs/loop_true-unreach-call.c timeout 900     270 10000    0 timeout 900     400   11000    0 out of memory 360    15000 5300    0 unknown .21  7.8 2.3  0 timeout 900   4400 6700 0 timeout 900   2500 7200 0 timeout 900   3700 8200 0 unknown 890    320 9200   0 true .25 40 2.8 2 timeout 900     2700 12000    0 out of memory 370     15000 4900    0 timeout 900     660 9700    0 error (1) 890     1100   9700    0 true 11     770   180    2 timeout 900   880 9200 0 error 74   410 850 0 timeout 900   1200 12000 0
float-benchs/mea8000_true-unreach-call.c timeout 900     2100 7400    0 timeout 900     27   12000    0 error (134) 190    13000 2000    0 out of memory 480     15000   6700    0 timeout 900   4600 11000 0 timeout (assertion) 900   7200 7700 0 timeout 970   11000 5800 0 unknown 890    2000 8500   0 true 310    7000 3500   2 timeout 900     1100 12000    0 out of memory 340     15000 4100    0 timeout 900     2100 8800    0 error (1) .46  58   5.4  0 timeout (timeout) 900     320   10000    0 unknown 5.1 310 43 0 unknown 5.0 310 36 0 unknown 4.6 300 36 0
float-benchs/nan_double_range_true-unreach-call.c true .11  22 .97 2 timeout 900     25   14000    0 true .22 30 1.6  2 true .14  43   .92 2 true 2.8 270 24 2 true 3.5 310 28 2 true 2.8 260 24 2 true 3.8  290 35   2 true .20 24 2.3 2 out of memory 57     15000 630    0 true .28  23 .72 2 true .085 23 .82 2 true .79  56   9.3  2 unknown .17  9.4 1.6  0 true 10   340 80 2 true 9.9 350 75 2 true 9.6 310 70 2
float-benchs/nan_float_range_true-unreach-call.c true .13  22 .77 2 timeout 900     25   11000    0 true .18 17 1.5  2 true .16  7.7 1.7  2 true 2.7 260 25 2 true 3.4 290 27 2 true 3.0 280 28 2 true 3.8  280 35   2 true .19 24 2.5 2 out of memory 79     15000 1100    0 true .12  23 .88 2 true .096 23 2.5  2 true .84  60   8.7  2 unknown .14  9.3 1.6  0 true 11   330 93 2 true 10   310 93 2 true 12   340 100 2
float-benchs/rlim_exit_true-unreach-call.c timeout 900     1700 12000    0 timeout 900     25   12000    0 error (134) 140    14000 1600    0 true 850     380   10000    2 timeout 900   4100 10000 0 timeout 900   3700 10000 0 timeout 900   3000 8200 0 unknown 890    220 12000   0 true 11    3600 120   2 timeout 900     590 9200    0 out of memory 430     15000 5600    0 timeout 900     340 9300    0 error (1) 890     290   9400    0 timeout (timeout) 900     41   13000    0 timeout 900   2200 13000 0 timeout 900   4900 15000 0 timeout 900   2000 12000 0
float-benchs/rlim_invariant_true-unreach-call.c timeout 900     1500 13000    0 timeout 900     25   11000    0 error (42) 850    1300 6500    0 true 850     410   10000    2 true 3.5 270 33 2 true 15   670 98 2 true 8.2 500 62 2 unknown 890    450 9300   0 true 12    3800 120   2 timeout 900     170 10000    0 timeout 900     200 10000    0 timeout 900     250 13000    0 true 540     1000   4700    2 timeout (timeout) 900     41   11000    0 timeout 900   1000 11000 0 error 73   430 820 0 timeout 900   730 12000 0
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c timeout 900     700 8200    0 timeout 900     25   13000    0 error (1) 850    310 9500    0 true .018 8.0 .20 2 error 2.8 280 25 0 error 5.3 310 40 0 unknown 5.3 330 42 0 unknown 890    1700 7700   0 unknown 900    3200 5000   0 timeout 900     2200 5000    0 timeout 900     2200 5600    0 timeout 900     2200 5500    0 error (1) 890     1200   10000    0 unknown .18  9.3 1.9  0 timeout 900   8100 8700 0 error 6.3 350 51 0 timeout 900   8100 7800 0
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c timeout 900     700 7500    0 timeout 900     25   14000    0 error (1) 850    310 8600    0 true .026 7.9 .15 2 error 2.5 270 21 0 error 5.8 340 43 0 unknown 5.4 310 48 0 unknown 890    1700 6400   0 unknown 900    4400 6700   0 timeout 900     2400 7000    0 timeout 900     2500 7700    0 timeout 900     2500 8100    0 error (1) 890     1200   7700    0 unknown .16  9.3 1.7  0 timeout 900   8100 8400 0 error 5.5 310 40 0 timeout 900   8100 6300 0
float-benchs/sin_interpolated_index_true-unreach-call.c timeout 900     700 7200    0 timeout 900     27   12000    0 error (1) 850    280 10000    0 true .038 7.8 .14 2 error 3.4 310 31 0 error 420   640 4900 0 unknown 420   540 5300 0 unknown 890    480 7900   0 unknown 900    650 6900   0 timeout 900     930 7800    0 timeout 900     940 8300    0 timeout 900     940 11000    0 error (1) 890     720   7200    0 unknown .16  9.3 1.9  0 out of memory 200   15000 2000 0 error 5.9 330 43 0 out of memory 200   15000 2200 0
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 900     440 7000    0 timeout 900     25   13000    0 error (42) 850    4400 5900    0 true .027 12   .25 2 error 2.5 270 23 0 error 29   2300 210 0 unknown 8.8 460 75 0 unknown 890    2100 7500   0 true 92    1700 870   2 timeout 900     2100 5900    0 timeout 900     2100 6200    0 timeout 900     2100 6500    0 out of memory 41     15000   480    0 unknown .18  9.3 1.7  0 timeout 900   8700 9900 0 error 5.5 320 42 0 timeout 900   8200 6300 0
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 900     320 8400    0 timeout 900     25   11000    0 error (42) 850    3100 7100    0 true .025 7.8 .15 2 error 2.6 270 24 0 error 30   2100 250 0 unknown 6.7 440 54 0 unknown 890    1800 6200   0 true 530    13000 4300   2 timeout 900     2200 7100    0 timeout 900     2200 6100    0 timeout 900     2200 6000    0 out of memory 38     15000   400    0 unknown .16  9.5 2.1  0 timeout 900   8700 6800 0 error 5.5 330 43 0 timeout 900   8800 7100 0
float-benchs/sqrt_Householder_constant_true-unreach-call.c timeout 900     240 8000    0 timeout 900     25   13000    0 true 1.2  19 13    2 unknown 23     6100   300    0 true 8.3 440 68 2 true 5.2 290 36 2 true 3.4 260 28 2 unknown 890    1000 8800   0 true .35 27 4.5 2 timeout 900     1600 14000    0 true .72  38 8.4  2 timeout 900     1000 7500    0 out of memory 40     15000   410    0 true .14  9.1 1.5  2 error 600   2900 5400 0 error 110   1500 880 0 error 330   3000 2800 0
float-benchs/sqrt_Householder_interval_true-unreach-call.c timeout 900     320 11000    0 timeout 900     25   11000    0 error (42) 850    580 7400    0 true 850     940   5400    2 error 15   650 150 0 timeout 900   2400 12000 0 timeout 900   3200 11000 0 unknown 890    620 7000   0 true 16    3600 180   2 timeout 900     770 7900    0 timeout 900     810 7000    0 timeout 900     810 7700    0 out of memory 41     15000   320    0 unknown .17  9.3 2.2  0 error 480   3000 3200 0 error 120   1500 1000 0 error 470   3000 3700 0
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c timeout 900     270 6600    0 timeout 900     25   13000    0 error (42) 850    3000 8900    0 true 850     1200   5600    2 error 14   640 160 0 timeout 900   2300 10000 0 timeout 900   3800 9300 0 unknown 890    1300 10000   0 true 50    3600 690   2 timeout 900     1200 3200    0 timeout 900     1200 2500    0 timeout 900     1300 7700    0 out of memory 41     15000   350    0 unknown .16  9.5 1.9  0 error 480   2800 3600 0 error 130   1900 1200 0 error 470   2800 4300 0
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c timeout 900     330 6200    0 exception (gremlins) .067 20   .81 0 error (42) 850    2000 7600    0 true 850     720   6500    2 error 14   640 150 0 timeout 900   3400 11000 0 timeout 900   4900 10000 0 unknown 890    1100 7900   0 true 50    3600 630   2 timeout 900     1100 8700    0 timeout 900     1100 9500    0 timeout 900     1100 7800    0 out of memory 39     15000   460    0 unknown .18  9.4 1.8  0 error 170   1700 1300 0 error 130   1700 1100 0 error 470   2800 3600 0
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c timeout 900     380 6600    0 exception (gremlins) .068 21   .68 0 error (42) 850    3300 7800    0 true 850     1400   8500    2 error 14   630 170 0 timeout 900   2300 9000 0 timeout 900   3000 8600 0 unknown 890    1400 8300   0 true 61    4400 740   2 timeout 900     1400 7400    0 timeout 900     1500 8300    0 timeout 900     1500 9400    0 out of memory 40     15000   360    0 unknown .16  9.4 1.8  0 error 450   2800 3100 0 error 130   1700 1300 0 error 440   2800 3500 0
float-benchs/sqrt_poly_true-unreach-call.c true 1.1   48 13    2 timeout 900     25   11000    0 true 3.0  55 42    2 true 20     85   270    2 error 49   660 470 0 true 160   820 1400 2 true 31   590 320 2 unknown 890    490 11000   0 true 11    300 100   2 timeout 900     490 10000    0 timeout 900     490 8800    0 timeout 900     490 6500    0 true 750     520   5900    2 unknown .15  9.5 1.8  0 true 580   1900 5700 2 error 98   760 1000 0 true 580   1900 4100 2
float-benchs/water_pid_true-unreach-call.c timeout 900     1100 12000    0 timeout 900     25   12000    0 true 1.4  18 14    2 out of memory 22     15000   250    0 error 250   6500 2600 0 true 6.9 410 50 2 true 4.0 270 36 2 unknown 890    580 7800   0 true .27 29 3.3 2 timeout 900     5200 12000    0 true 3.9   140 57    2 timeout 900     850 7800    0 error (1) 890     9000   8800    0 true .16  9.2 1.4  2 error 420   3500 3700 0 error 34   1200 260 0 error 360   3100 3400 0
float-benchs/zonotope_2_true-unreach-call.c timeout 900     890 7900    0 exception (gremlins) .16  25   2.0  0 true 120    4700 1200    2 true .036 7.8 .13 2 true 3.8 290 33 2 timeout 900   3100 6200 0 timeout 900   3000 8100 0 unknown 44    76 590   0 true .53 81 5.9 2 timeout 900     6000 12000    0 out of memory 580     15000 7700    0 timeout 900     1200 8700    0 true 260     470   3000    2 true 1.0   56   13    2 timeout 900   1300 9200 0 timeout 900   860 8200 0 timeout 900   1700 6800 0
float-benchs/zonotope_3_true-unreach-call.c timeout 900     1400 11000    0 timeout 900     25   12000    0 error (134) 140    14000 1800    0 true .024 7.8 .14 2 timeout 900   4000 12000 0 true 13   570 77 2 true 160   2300 1700 2 true 210    1800 2300   2 true 11    3600 130   2 timeout 900     950 11000    0 out of memory 480     15000 5500    0 true 23     110 250    2 true 22     310   220    2 timeout (timeout) 900     41   11000    0 timeout 900   5400 14000 0 timeout 900   5300 12000 0 timeout 900   5400 13000 0
float-benchs/zonotope_loose_true-unreach-call.c true .38  30 4.3  2 false(unreach-call) .074 22   .81 -16 true .41 28 4.5  2 true 13     79   150    2 error 4.4 360 42 0 true 5.5 390 43 2 true 4.9 350 42 2 true 92    350 1000   2 true 2.1  110 21   2 timeout 900     1200 10000    0 true 39     150 480    2 true 40     150 530    2 true 8.9   210   73    2 unknown .16  9.4 1.9  0 true 590   1300 4000 2 error 84   690 830 0 true 640   1400 4500 2
float-benchs/zonotope_tight_true-unreach-call.c true .22  30 1.9  2 false(unreach-call) .068 21   .66 -16 true .42 30 4.6  2 true 14     79   180    2 error 4.4 360 41 0 true 5.5 380 41 2 true 4.9 340 49 2 true 110    350 1000   2 true 2.1  110 26   2 timeout 900     1000 8300    0 true 54     150 480    2 true 52     150 480    2 true 12     220   110    2 unknown .18  9.4 1.9  0 true 550   1300 5100 2 error 75   710 670 0 true 650   1400 4200 2
floats-esbmc-regression/Double_div_true-unreach-call.i true 2.9   46 41    2 exception (gremlins) .074 22   .58 0 true 2.3  18 26    2 true .055 7.9 .47 2 timeout 900   4200 11000 0 true 6.0 470 46 2 true 5.5 410 46 2 unknown 890    270 6500   0 true .22 30 2.3 2 timeout 900     2400 11000    0 true 34     980 460    2 timeout 900     510 9300    0 error (1) 890     12000   8600    0 true .13  9.5 1.7  2 true 540   2600 4600 2 error 38   710 370 0 true 600   2400 5000 2
floats-esbmc-regression/Float_div_true-unreach-call.i true .70  30 8.1  2 exception (gremlins) .081 20   .65 0 true 1.0  17 10    2 true .11  14   .51 2 timeout 900   4200 11000 0 true 3.9 290 30 2 true 3.1 270 27 2 unknown 890    670 8300   0 true .15 23 1.7 2 timeout 900     4700 12000    0 true .57  54 7.9  2 timeout 900     1200 8100    0 true 680     2000   7100    2 true .13  9.4 1.6  2 true 460   780 4800 2 error 72   410 640 0 true 220   520 1800 2
floats-esbmc-regression/ceil_nondet_true-unreach-call.i true 3.2   71 40    2 false(unreach-call) .077 22   .83 -16 true 6.1  47 76    2 true .11  8.2 1.5  2 error 3.2 290 25 0 error 6.7 450 49 0 unknown 6.5 420 52 0 unknown 17    450 170   0 true .58 44 7.7 2 timeout 900     4800 11000    0 true 15     70 29    2 true 4.0   70 58    2 error (1) .072 7.3 .39 0 unknown .098 9.4 .71 0 unknown 9.0 330 71 0 unknown 8.4 300 67 0 unknown 9.0 320 76 0
floats-esbmc-regression/ceil_true-unreach-call.i true .49  31 3.8  2 false(unreach-call) .071 21   .71 -16 true .76 23 6.2  2 true .061 8.2 .55 2 true 4.4 290 37 2 true 3.5 270 28 2 true 2.8 260 27 2 true 4.3  270 39   2 true .32 26 4.0 2 out of memory 150     15000 1600    0 true .13  26 1.5  2 true .15  26 1.7  2 error (1) .61  44   8.0  0 unknown .13  9.6 1.4  0 unknown 5.0 300 40 0 unknown 4.8 300 41 0 unknown 5.3 310 38 0
floats-esbmc-regression/copysign_true-unreach-call.i true .36  29 2.6  2 false(unreach-call) .070 22   .81 -16 true .55 23 5.6  2 true .10  8.3 .56 2 true 4.4 290 37 2 true 3.6 280 28 2 true 3.0 260 24 2 true 4.6  320 38   2 true .25 27 3.1 2 timeout 900     8700 10000    0 true .14  26 1.5  2 true .16  26 1.4  2 true .89  63   10    2 unknown .14  9.6 1.6  0 unknown 5.1 300 42 0 unknown 4.9 300 40 0 unknown 5.0 300 35 0
floats-esbmc-regression/digits_for_true-unreach-call.i timeout 900     510 7900    0 exception (gremlins) .083 23   .66 0 true 1.0  17 14    2 true .056 7.8 .57 2 error 7.1 460 53 0 true 3.4 280 27 2 true 2.7 250 19 2 true 32    260 270   2 true .15 23 1.7 2 timeout 900     1800 13000    0 true .40  29 4.3  2 timeout 900     2200 9400    0 true .85  60   11    2 true .16  9.4 1.4  2 timeout 900   1500 7500 0 error 4.7 310 39 0 timeout 900   4700 7200 0
floats-esbmc-regression/digits_while_true-unreach-call.i timeout 900     520 8500    0 exception (gremlins) .071 21   .74 0 true 1.1  17 10    2 true .058 7.7 .48 2 error 7.7 470 55 0 true 3.4 270 28 2 true 2.5 250 23 2 true 31    260 330   2 true .16 23 1.8 2 timeout 900     1800 12000    0 true .37  29 4.5  2 timeout 900     2200 7400    0 true .81  55   9.1  2 true .15  9.3 1.8  2 timeout 900   3100 8000 0 error 5.1 310 39 0 timeout 900   3600 7900 0
floats-esbmc-regression/fabs_true-unreach-call.i true .22  28 2.0  2 false(unreach-call) .079 21   .66 -16 true .37 21 2.9  2 true .064 7.9 .58 2 true 3.9 290 32 2 true 5.0 280 37 2 true 4.2 300 35 2 true 5.8  300 50   2 true .26 27 2.9 2 timeout 900     9400 11000    0 true .13  26 1.4  2 true .15  26 1.4  2 true .83  60   11    2 unknown .14  9.6 1.5  0 true 10   300 80 2 true 9.4 310 70 2 true 10   310 75 2
floats-esbmc-regression/fdim_true-unreach-call.i true .24  29 1.9  2 false(unreach-call) .065 21   .65 -16 true .37 22 4.3  2 true .068 8.0 .57 2 true 4.0 290 32 2 true 3.4 270 27 2 true 2.9 250 26 2 true 4.4  270 43   2 true .27 26 2.4 2 timeout 900     10000 12000    0 true .12  26 1.6  2 true .12  26 1.2  2 true .80  64   11    2 unknown .15  9.5 1.3  0 unknown 6.4 360 48 0 unknown 5.0 300 38 0 unknown 5.8 330 42 0
floats-esbmc-regression/floor_nondet_true-unreach-call.i true 3.2   73 42    2 false(unreach-call) .077 23   .87 -16 true 6.5  49 84    2 true .13  8.1 1.2  2 error 3.2 280 29 0 error 6.6 450 50 0 unknown 6.2 450 54 0 unknown 14    420 150   0 true .59 44 6.6 2 timeout 900     6700 11000    0 true 2.9   68 35    2 true 2.9   68 37    2 error (1) .058 7.1 .30 0 unknown .098 9.5 .78 0 unknown 8.9 320 71 0 unknown 8.4 310 65 0 unknown 8.6 310 72 0
floats-esbmc-regression/floor_true-unreach-call.i true .44  31 4.9  2 false(unreach-call) .11  17   .57 -16 true .78 23 6.8  2 true .078 8.2 .53 2 true 4.5 280 35 2 true 3.5 270 29 2 true 2.8 270 26 2 true 4.4  280 42   2 true .33 26 3.7 2 out of memory 150     15000 2100    0 true .13  26 1.3  2 true .16  26 1.3  2 error (1) .61  45   6.2  0 unknown .12  9.6 1.8  0 unknown 5.7 320 38 0 unknown 5.1 300 38 0 unknown 5.1 300 37 0
floats-esbmc-regression/fmax_true-unreach-call.i true .32  31 3.7  2 false(unreach-call) .067 22   .78 -16 true .58 22 5.1  2 true .097 8.1 .55 2 true 4.0 280 35 2 true 3.7 270 29 2 true 2.8 260 26 2 true 4.1  260 43   2 true .27 27 2.2 2 timeout 900     11000 14000    0 true .12  26 1.3  2 true .12  26 1.4  2 true .82  60   8.6  2 unknown .12  9.6 1.3  0 unknown 6.2 320 52 0 unknown 4.9 330 34 0 unknown 5.1 300 38 0
floats-esbmc-regression/fmin_true-unreach-call.i true .35  30 3.0  2 false(unreach-call) .070 22   .88 -16 true .54 22 5.0  2 true .076 8.0 .58 2 true 3.9 280 33 2 true 3.5 290 31 2 true 2.8 260 21 2 true 4.3  270 43   2 true .23 27 2.4 2 timeout 900     11000 12000    0 true .12  26 1.4  2 true .12  26 1.3  2 true .83  54   11    2 unknown .12  9.5 1.5  0 unknown 5.2 310 43 0 unknown 5.4 300 39 0 unknown 5.1 310 38 0
floats-esbmc-regression/fmod2_true-unreach-call.i true .91  76 12    2 false(unreach-call) .076 23   .98 -16 true .94 23 7.9  2 true .11  8.2 1.1  2 false(unreach-call) 4.6 300 39 -16 false(unreach-call) 6.0 330 43 -16 false(unreach-call) 3.8 270 35 -16 false(unreach-call) 5.4  290 46   -16 true .34 27 4.6 2 out of memory 1.9   15000 26    0 true .22  880 2.3  2 true .25  890 2.7  2 out of memory 36     15000   450    0 unknown .14  9.6 1.7  0 unknown 9.6 330 73 0 unknown 8.8 320 70 0 unknown 9.2 320 70 0
floats-esbmc-regression/fmod3_true-unreach-call.i true .96  79 9.0  2 false(unreach-call) .076 21   .81 -16 true .98 23 7.7  2 true .11  8.0 1.0  2 false(unreach-call) 5.0 320 42 -16 false(unreach-call) 5.6 310 39 -16 false(unreach-call) 3.5 270 33 -16 false(unreach-call) 4.9  280 45   -16 true .34 26 4.1 2 out of memory 1.9   15000 27    0 true .22  880 2.6  2 true .84  880 2.6  2 out of memory 37     15000   470    0 unknown .14  9.4 2.1  0 unknown 9.2 330 79 0 unknown 8.4 310 66 0 unknown 8.8 310 69 0
floats-esbmc-regression/fmod_true-unreach-call.i true .89  63 8.0  2 false(unreach-call) .11  17   .51 -16 true .97 23 7.9  2 true .058 8.0 .59 2 true 4.6 290 35 2 true 3.6 270 28 2 true 2.8 260 23 2 true 4.2  270 42   2 true .23 27 3.0 2 timeout 900     7100 11000    0 true .15  26 1.4  2 true .15  26 1.5  2 error (1) .62  41   8.2  0 true .13  9.7 1.7  2 unknown 5.8 320 41 0 unknown 5.5 300 38 0 unknown 5.3 320 42 0
floats-esbmc-regression/isgreater_true-unreach-call.i true .21  28 1.6  2 false(unreach-call) .067 21   .72 -16 true .36 21 3.2  2 true .059 8.1 .60 2 true 4.2 300 30 2 true 3.5 270 27 2 true 2.8 260 23 2 true 4.3  270 40   2 true .23 27 3.2 2 timeout 900     15000 12000    0 true .12  26 1.5  2 true .12  26 1.4  2 true .83  60   9.1  2 true .14  9.4 1.5  2 error 8.8 330 67 0 error 8.3 300 75 0 error 8.8 310 76 0
floats-esbmc-regression/isgreaterequal_true-unreach-call.i true .21  28 1.5  2 false(unreach-call) .083 18   .77 -16 true .36 34 3.4  2 true .066 8.2 .51 2 true 4.0 290 39 2 true 3.7 280 29 2 true 2.9 250 25 2 true 4.2  270 43   2 true .24 26 2.7 2 timeout 900     14000 12000    0 true .15  26 1.1  2 true .12  26 1.4  2 true .80  57   8.3  2 true .15  9.5 1.5  2 error 8.7 300 68 0 error 8.2 310 62 0 error 9.7 320 72 0
floats-esbmc-regression/isless_true-unreach-call.i true .21  28 1.9  2 false(unreach-call) .068 22   .76 -16 true .36 21 3.1  2 true .11  27   .68 2 true 4.1 290 35 2 true 3.5 270 29 2 true 2.7 260 25 2 true 4.2  270 41   2 true .23 27 2.8 2 timeout 900     15000 11000    0 true .13  26 1.4  2 true .12  26 1.2  2 true .84  56   9.2  2 true .16  9.5 1.5  2 error 8.2 300 61 0 error 8.8 310 67 0 error 8.8 310 70 0
floats-esbmc-regression/islessequal_true-unreach-call.i true .23  28 1.4  2 false(unreach-call) .072 24   .66 -16 true .33 21 4.3  2 true .070 8.2 .64 2 true 4.3 290 34 2 true 3.5 270 31 2 true 2.8 270 26 2 true 4.4  270 39   2 true .24 27 2.7 2 timeout 900     14000 11000    0 true .12  26 1.3  2 true .15  26 1.1  2 true .83  55   9.5  2 true .13  9.4 1.3  2 error 9.0 340 70 0 error 9.7 350 78 0 error 8.6 300 63 0
floats-esbmc-regression/islessgreater_true-unreach-call.i true .21  28 2.1  2 false(unreach-call) .071 22   .78 -16 true .33 21 3.4  2 true .067 8.0 .50 2 true 4.3 290 33 2 true 3.6 280 30 2 true 2.7 260 24 2 true 4.1  270 41   2 true .25 27 2.5 2 timeout 900     13000 12000    0 true .15  26 1.3  2 true .14  26 1.2  2 true .83  58   9.6  2 true .14  9.5 1.6  2 error 9.1 320 63 0 error 8.6 320 76 0 error 9.4 350 73 0
floats-esbmc-regression/isunordered_true-unreach-call.i true .28  28 2.7  2 false(unreach-call) .064 22   .78 -16 true .54 22 7.0  2 true .082 17   .56 2 true 3.9 280 38 2 true 3.4 270 27 2 true 2.8 250 21 2 true 4.1  260 44   2 true .26 27 2.4 2 timeout 900     13000 11000    0 true .15  26 1.2  2 true .13  26 1.4  2 true .80  59   10    2 true .14  9.4 1.6  2 error 9.8 330 69 0 error 8.8 320 62 0 error 8.9 320 76 0
floats-esbmc-regression/lrint_true-unreach-call.i true .51  30 3.9  2 false(unreach-call) .073 21   .83 -16 true .73 23 9.7  2 true .092 14   .64 2 error 3.2 290 30 0 error 7.5 460 54 0 unknown 6.5 430 44 0 unknown 8.7  480 78   0 true .38 26 4.3 2 out of memory 7.6   15000 21    0 true .24  880 3.1  2 true .26  880 2.9  2 error (1) .063 7.5 .39 0 unknown .074 9.5 .76 0 unknown 5.8 320 43 0 unknown 5.5 320 45 0 unknown 5.3 300 39 0
floats-esbmc-regression/modf_true-unreach-call.i true .41  30 3.1  2 false(unreach-call) .070 21   .68 -16 true .78 23 7.7  2 true .13  8.1 1.1  2 error 3.3 280 29 0 true 3.5 270 31 2 true 2.8 250 21 2 true 4.2  270 46   2 true .32 26 4.7 2 out of memory 140     15000 1800    0 true .15  26 1.6  2 true .15  26 1.4  2 true 9.9   170   100    2 unknown .15  9.5 1.4  0 unknown 6.0 330 40 0 unknown 4.9 310 35 0 unknown 5.3 310 41 0
floats-esbmc-regression/nan_true-unreach-call.i true .27  30 2.5  2 false(unreach-call) .067 22   .68 -16 true .39 22 3.6  2 true .12  8.3 1.2  2 true 4.1 290 34 2 true 3.5 270 25 2 true 2.9 260 21 2 true 4.1  270 40   2 true .26 27 2.8 2 timeout 900     11000 11000    0 true .12  26 1.5  2 true .12  26 1.2  2 true .85  62   9.6  2 unknown .12  9.5 1.5  0 true 9.9 310 84 2 true 11   310 82 2 true 11   310 91 2
floats-esbmc-regression/nearbyint2_true-unreach-call.i true .53  31 4.2  2 false(unreach-call) .070 21   .77 -16 true .80 23 7.8  2 true .085 8.2 .45 2 error 3.1 280 26 0 error 7.7 450 60 0 unknown 7.3 440 55 0 unknown 9.1  440 74   0 true .38 26 4.2 2 out of memory 190     15000 2200    0 true .14  26 1.7  2 true .16  26 1.8  2 error (1) .078 7.3 .40 0 unknown .10  9.7 .85 0 unknown 6.3 330 48 0 unknown 5.0 300 37 0 unknown 6.0 330 47 0
floats-esbmc-regression/nearbyint_true-unreach-call.i true .46  31 6.0  2 false(unreach-call) .070 18   .86 -16 true 1.6  23 14    2 true .12  28   .64 2 error 3.2 270 25 0 error 11   520 72 0 unknown 9.0 460 73 0 unknown 11    470 91   0 true .37 26 3.9 2 out of memory 240     15000 2900    0 true .17  26 2.3  2 true .60  37 7.4  2 error (1) .076 7.5 .52 0 unknown .076 9.5 .85 0 unknown 6.2 350 46 0 unknown 5.1 320 37 0 unknown 5.3 320 44 0
floats-esbmc-regression/remainder_true-unreach-call.i true 1.1   86 10    2 timeout 900     27   11000    0 true .96 23 8.6  2 true .11  8.1 .47 2 false(unreach-call) 4.2 300 39 -16 true 3.8 270 28 2 true 2.8 260 25 2 true 4.5  270 51   2 true .37 26 4.0 2 out of memory 2.0   15000 24    0 true .27  890 3.0  2 true .26  880 2.6  2 error (1) .077 7.3 .43 0 unknown .13  9.5 1.5  0 unknown 5.0 310 42 0 unknown 5.2 320 40 0 unknown 5.5 310 39 0
floats-esbmc-regression/rint2_true-unreach-call.i true .50  31 4.4  2 false(unreach-call) .088 17   .71 -16 true .78 23 7.1  2 true .068 8.1 .58 2 error 3.1 270 24 0 error 8.0 460 61 0 unknown 7.2 440 57 0 unknown 9.3  320 86   0 true .40 26 4.6 2 out of memory 220     15000 2700    0 true .18  26 1.5  2 true .17  26 1.7  2 error (1) .063 7.5 .44 0 unknown .075 9.5 .71 0 unknown 5.0 320 41 0 unknown 5.0 300 39 0 unknown 5.1 310 38 0
floats-esbmc-regression/rint_true-unreach-call.i true .51  31 4.3  2 false(unreach-call) .072 20   .81 -16 true 1.6  23 13    2 true .084 15   .98 2 error 3.4 280 32 0 error 11   520 84 0 unknown 8.3 470 64 0 unknown 11    470 91   0 true .40 26 4.3 2 out of memory 260     15000 3600    0 true .20  27 1.9  2 true .47  36 6.1  2 error (1) .063 7.5 .53 0 unknown .094 9.5 .79 0 unknown 5.4 310 44 0 unknown 5.2 300 42 0 unknown 5.3 320 41 0
floats-esbmc-regression/round_nondet_true-unreach-call.i true 3.6   100 44    2 false(unreach-call) .076 18   .87 -16 true 5.9  67 76    2 true .11  8.0 1.5  2 error 3.1 270 27 0 error 7.4 450 59 0 unknown 6.5 440 46 0 unknown 17    440 170   0 true 1.3  87 15   2 timeout 900     3200 10000    0 true 13     120 140    2 true 12     120 120    2 error (1) .062 7.2 .33 0 unknown .074 9.6 .84 0 unknown 8.6 300 69 0 unknown 9.1 320 74 0 unknown 8.4 310 74 0
floats-esbmc-regression/round_true-unreach-call.i true .53  35 5.8  2 false(unreach-call) .096 23   .71 -16 true .78 24 9.7  2 true .064 8.2 .52 2 true 5.5 350 46 2 true 3.8 280 31 2 true 2.9 260 24 2 true 20    270 32   2 true .42 28 4.9 2 out of memory 2.3   15000 33    0 true .28  890 3.0  2 true .27  890 3.2  2 error (1) .61  38   8.8  0 unknown .13  9.5 1.5  0 unknown 5.6 320 45 0 unknown 5.2 300 42 0 unknown 5.2 300 38 0
floats-esbmc-regression/rounding_functions_true-unreach-call.i true .52  31 5.2  2 false(unreach-call) .12  23   .62 -16 true .85 23 7.1  2 true .064 8.3 .50 2 true 5.6 410 46 2 true 4.3 300 36 2 true 2.9 250 27 2 true 5.1  260 51   2 true .47 29 6.8 2 out of memory 440     15000 5400    0 true .20  28 2.3  2 true .20  28 2.3  2 true 1.2   150   14    2 unknown .13  9.5 1.3  0 unknown 5.1 310 38 0 unknown 5.0 300 40 0 unknown 5.4 320 42 0
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i true 1.9   35 23    2 false(unreach-call) .079 21   .97 -16 true 4.0  31 51    2 true .11  7.9 1.2  2 false(unreach-call) 4.7 310 41 -16 false(unreach-call) 5.6 310 38 -16 false(unreach-call) 3.5 280 31 -16 unknown 890    97 12000   0 true 2.3  47 27   2 timeout 900     3200 11000    0 true 290     960 3000    2 true 290     970 3500    2 error (1) .066 7.5 .34 0 unknown .14  9.5 1.8  0 unknown 8.3 300 73 0 unknown 9.6 330 82 0 unknown 8.2 310 65 0
floats-esbmc-regression/trunc_nondet_true-unreach-call.i true 2.4   74 34    2 false(unreach-call) .076 23   .88 -16 true 3.7  46 40    2 true .12  8.0 1.1  2 error 3.0 270 28 0 error 6.4 450 46 0 unknown 6.7 450 57 0 unknown 12    430 110   0 true .61 44 7.0 2 timeout 900     9600 11000    0 true 1.8   59 25    2 true 1.8   60 21    2 error (1) .071 7.2 .37 0 unknown .10  9.5 .91 0 unknown 8.9 310 70 0 unknown 9.3 330 78 0 unknown 8.5 310 69 0
floats-esbmc-regression/trunc_true-unreach-call.i true .48  31 4.2  2 false(unreach-call) .067 22   .80 -16 true .81 23 6.3  2 true .097 8.2 .46 2 true 4.7 280 35 2 true 3.6 270 30 2 true 3.1 280 25 2 true 4.4  300 43   2 true .32 26 3.7 2 out of memory 160     15000 1600    0 true .13  26 1.6  2 true .13  26 1.6  2 error (1) .59  43   6.4  0 unknown .13  9.4 1.5  0 unknown 5.4 320 38 0 unknown 5.4 320 39 0 unknown 5.2 310 35 0
floats-esbmc-regression/Double_div_bad_false-unreach-call.i timeout 900     490 11000    0 false(unreach-call) .065 21   .64 1 false(unreach-call) 4.8  31 49    1 false(unreach-call) .057 7.8 .60 1 timeout 900   4100 10000 0 timeout 900   2300 8800 0 false(unreach-call) 74   2900 820 1 unknown 890    640 10000   0 false(unreach-call) .20 23 2.1 1 false(unreach-call) 61     320 860    1 false(unreach-call) 130     3300 1700    1 timeout 900     1400 8700    0 error (1) 890     12000   11000    0 false(unreach-call) .17  12   1.8  1 error 14   570 150 0 error 60   860 670 0 error 14   560 120 0
floats-esbmc-regression/Float_div_bad_false-unreach-call.i timeout 900     330 11000    0 false(unreach-call) .088 21   .62 1 false(unreach-call) 1.1  17 13    1 false(unreach-call) .053 8.0 .48 1 timeout 900   4100 12000 0 false(unreach-call) 11   530 83 1 false(unreach-call) 8.5 470 66 1 unknown 890    650 7900   0 false(unreach-call) .14 23 1.8 1 false(unreach-call) .84  25 12    1 false(unreach-call) 1.7   120 25    1 timeout 900     1600 9400    0 error (1) 890     2200   8900    0 false(unreach-call) .14  9.4 1.7  1 timeout 900   1400 8400 0 error 79   450 760 0 timeout 900   1900 6200 0
floats-esbmc-regression/digits_bad_for_false-unreach-call.i timeout 900     450 7600    0 exception (gremlins) .11  21   .59 0 false(unreach-call) .98 17 10    1 false(unreach-call) .11  64   1.1  1 error 8.8 460 66 0 false(unreach-call) 7.1 400 44 1 false(unreach-call) 4.2 280 35 1 false(unreach-call) 24    270 230   1 false(unreach-call) .15 23 1.8 1 false(unreach-call) .21  23 2.8  1 false(unreach-call) .37  27 5.0  1 timeout 900     2100 8600    0 false(unreach-call) .91  70   9.7  1 false(unreach-call) .16  9.3 1.4  1 timeout 900   1300 7800 0 error 5.2 310 40 0 timeout 900   5700 8100 0
floats-esbmc-regression/digits_bad_while_false-unreach-call.i timeout 900     450 7500    0 exception (gremlins) .069 20   .91 0 false(unreach-call) .97 17 9.2  1 false(unreach-call) .045 7.8 .77 1 error 7.8 470 63 0 false(unreach-call) 8.6 470 57 1 false(unreach-call) 4.3 270 35 1 false(unreach-call) 26    280 210   1 false(unreach-call) .18 23 1.5 1 false(unreach-call) .23  23 4.9  1 false(unreach-call) .37  27 4.6  1 timeout 900     2200 8300    0 false(unreach-call) .85  62   10    1 false(unreach-call) .13  9.3 1.8  1 timeout 900   2000 9200 0 error 4.9 310 38 0 timeout 900   4300 7600 0
../../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 172 38000 37000 390000 248 172 59000    3800 800000   -573 172 22000 100000 200000 264 172 16000 110000 160000 298 172 30000   520000 270000 -56 172 43000 420000 300000 107 172 38000 290000 320000 129 172 70000 89000 660000 100 172 7900 120000 63000 308 172 120000 800000 1400000 18 172 61000 190000 530000 194 172 73000 96000 630000 173 172 51000 340000 450000 153 172 13000    33000 150000 86 172 46000 630000 420000 109 172 12000 120000 130000 62 172 46000 640000 410000 109
    correct results 137 6400 12000 64000 248 11 2.3  230 24   19 147 3000 14000 30000 264 164 15000 32000 150000 298 78 1400   49000 12000 136 107 5700 79000 37000 187 111 4100 72000 33000 193 82 3800 25000 36000 148 169 5200 110000 45000 308 18 2400 3100 22000 18 106 5100 18000 47000 194 93 3300 11000 33000 173 86 5400 20000 50000 153 46 19    1300 260 86 63 5900 74000 52000 109 33 490 12000 4800 62 63 6400 74000 51000 109
        correct true 111 5100 9400 50000 222 8 2.0  160 22   16 117 2700 12000 27000 234 134 14000 13000 140000 268 58 240   18000 2000 116 80 1900 46000 14000 160 82 3300 56000 28000 164 66 1500 22000 16000 132 139 4800 110000 41000 278 0 88 2700 11000 23000 176 80 1800 9000 20000 160 67 3000 15000 29000 134 40 18    1200 250 80 46 4900 43000 44000 92 29 450 10000 4400 58 46 5400 43000 43000 92
        correct false 26 1300 2700 15000 26 3 .27 62 1.8 3 30 280 2000 2900 30 30 1700 19000 15000 30 20 1200   32000 9600 20 27 3800 33000 23000 27 29 730 16000 5800 29 16 2300 3000 20000 16 30 360 5200 3300 30 18 2400 3100 22000 18 18 2400 6100 24000 18 13 1500 2200 13000 13 19 2400 4600 21000 19 6 .96 61 10 6 17 1000 31000 8300 17 4 45 1300 420 4 17 1000 31000 8000 17
    correct-unconfimed results 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
    incorrect results 0 37 2.9  780 28   -592 0 0 9 34   2700 300 -192 5 27 1600 200 -80 4 14 1100 120 -64 3 330 830 2900 -48 0 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 3 8.1 840 75 -96 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 37 2.9  780 28   -592 0 0 6 26   1900 230 -96 5 27 1600 200 -80 4 14 1100 120 -64 3 330 830 2900 -48 0 0 0 0 0 0 0 0 0
score (172 tasks, max score: 314) 248 -573 264 298 -56 107 129 100 308 18 194 173 153 86 109 62 109
Run set 2ls.sv-comp17.ReachSafety-Floats blast.sv-comp17.ReachSafety-Floats cbmc.sv-comp17.ReachSafety-Floats ceagle.sv-comp17.ReachSafety-Floats cpa-bam-bnb.sv-comp17.ReachSafety-Floats cpa-kind.sv-comp17.ReachSafety-Floats cpa-seq.sv-comp17.ReachSafety-Floats depthk.sv-comp17.ReachSafety-Floats esbmc.sv-comp17.ReachSafety-Floats esbmc-falsi.sv-comp17.ReachSafety-Floats esbmc-incr.sv-comp17.ReachSafety-Floats esbmc-kind.sv-comp17.ReachSafety-Floats smack.sv-comp17.ReachSafety-Floats symbiotic4.sv-comp17.ReachSafety-Floats uautomizer.sv-comp17.ReachSafety-Floats ukojak.sv-comp17.ReachSafety-Floats utaipan.sv-comp17.ReachSafety-Floats