Tool VeriAbs CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon020; apollon077; apollon078; apollon084; apollon149; apollon164] apollon* [apollon037; apollon065; apollon077; apollon078; apollon155; apollon159] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 18:04:04 CET 2017-12-03 04:46:33 CET 2017-12-03 06:08:30 CET 2017-12-03 06:21:09 CET 2017-12-03 06:27:12 CET 2017-12-03 03:55:53 CET 2017-12-03 04:55:47 CET
Run set veriabs.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Floats
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 120   380 1100 false(unreach-call) 1 wit inspect 58    360 false(unreach-call) 1 wit inspect 47     680   unknown 0 wit inspect 2.0  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 75   380 650 false(unreach-call) 1 wit inspect 25    360 timeout 0 wit inspect 97     710   unknown 0 wit inspect 2.0  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 87   380 850 false(unreach-call) 1 wit inspect 18    360 false(unreach-call) 1 wit inspect 22     680   unknown 0 wit inspect 1.9  190 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 64   380 650 false(unreach-call) 1 wit inspect 51    360 false(unreach-call) 1 wit inspect 42     670   unknown 0 wit inspect 1.9  190 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 41   380 400 false(unreach-call) 1 wit inspect 11    360 false(unreach-call) 1 wit inspect 32     670   unknown 0 wit inspect 3.2  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i timeout 0 wit inspect 900   230 13000 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0047 .29 - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i timeout 0 wit inspect 900   230 13000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i timeout 0 wit inspect 900   230 11000 error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .026 5.0 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i timeout 0 wit inspect 900   230 11000 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i timeout 0 wit inspect 900   230 12000 error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i timeout 0 wit inspect 900   230 12000 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19   340 230 false(unreach-call) 1 wit inspect 9.2  310 false(unreach-call) 1 wit inspect 25     580   unknown 0 wit inspect 2.7  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 51   370 460 false(unreach-call) 1 wit inspect 53    330 false(unreach-call) 1 wit inspect 32     560   unknown 0 wit inspect 2.7  190 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 220   450 1800 true -32 wit inspect 2.0  250 timeout 0 wit inspect 97     610   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 32   350 400 false(unreach-call) 1 wit inspect 10    320 timeout 0 wit inspect 97     430   unknown 0 wit inspect 2.0  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 200   510 1600 false(unreach-call) 1 wit inspect 44    350 timeout 0 wit inspect 97     410   unknown 0 wit inspect 2.7  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 71   360 590 false(unreach-call) 1 wit inspect 19    330 timeout 0 wit inspect 97     440   unknown 0 wit inspect 2.7  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 2 wit inspect 190   380 2700 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .46 43 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.8
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .017 4.8
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .022 4.8
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .022 4.9
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   230 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8
floats-cdfpl/sine_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   160 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .022 4.9
floats-cdfpl/sine_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   160 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .020 4.9
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 2 wit inspect 200   370 2700 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    650 timeout 0 wit inspect 960     820  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 120   360 1500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 780    600 timeout 0 wit inspect 960     800  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i timeout 0 wit inspect 900   160 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/square_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   150 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 45 error (2) 0 wit inspect .029 4.9
floats-cdfpl/square_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   160 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .031 4.8
floats-cdfpl/square_6_true-unreach-call_true-termination.i timeout 0 wit inspect 900   160 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 5.0
floats-cdfpl/square_7_true-unreach-call_true-termination.i timeout 0 wit inspect 900   160 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .019 4.8
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 52   370 480 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 67    360 true 2 wit inspect 120     610  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 170   450 2100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  330 true 2 wit inspect 34     610  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i unknown 0 wit inspect 610   260 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .029 4.8
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 8.1 270 66 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 10     240  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 180   450 2600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    300 true 2 wit inspect 38     400  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 8.0 270 67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.3   220  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 17   370 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  270 true 2 wit inspect 39     580  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 7.8 280 64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 7.9 270 68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 9.2   250  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 15   280 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 12     300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect 170   370 2500 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.1  260 unknown 0 wit inspect 4.0   200  
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 170   300 2000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 true 2 wit inspect 140     450  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 8.3 280 82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 11     240  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 9.1 270 80 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 11     290  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 8.3 280 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 8.0 270 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 15     270  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 8.5 280 81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.1   250  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 15   280 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 9.2   290  
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 39   710 360 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 38    560 unknown 0 wit inspect 4.0   200  
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 20   290 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 true 2 wit inspect 11     280  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 7.8 270 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.4   240  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 10   270 90 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 25     390  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 170   570 2100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4  290 true 2 wit inspect 71     600  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect 12   320 100 - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 6.4  280 true 2 wit inspect 320     1100  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 7.9 270 74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.1  250 true 2 wit inspect 8.6   270  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 8.6 290 83 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 true 2 wit inspect 14     320  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 250   480 3000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 75    330 true 2 wit inspect 75     440  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 8.7 280 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 28     270  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 8.6 280 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.7  260 true 2 wit inspect 12     290  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 170   300 2200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    270 true 2 wit inspect 10     290  
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect 12   190 110 - wit inspect - wit inspect - wit inspect - wit inspect error (parsing failed) 0 wit inspect 2.2  140 error (7) 0 wit inspect 9.5   240  
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 16   310 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 17     530  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 11   290 100 false(unreach-call) 1 wit inspect 2.3  270 false(unreach-call) 1 wit inspect 12     280   unknown 0 wit inspect 2.8  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 11   290 92 false(unreach-call) 1 wit inspect 2.3  270 false(unreach-call) 1 wit inspect 10     270   unknown 0 wit inspect 2.1  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   290 94 false(unreach-call) 1 wit inspect 2.4  270 false(unreach-call) 1 wit inspect 12     280   unknown 0 wit inspect 2.1  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.4 290 70 false(unreach-call) 1 wit inspect 2.1  260 false(unreach-call) 1 wit inspect 11     300   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c unknown 0 wit inspect 110   220 1400 error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.5 290 61 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 9.5   280   unknown 0 wit inspect 2.8  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.3 270 70 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.1   220   unknown 0 wit inspect 2.7  190 true -32 wit inspect .59   18    - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.4 280 65 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.4   220   unknown 0 wit inspect 2.7  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 32   350 400 false(unreach-call) 1 wit inspect 5.2  320 false(unreach-call) 1 wit inspect 28     1200   unknown 0 wit inspect 3.0  210 true -32 wit inspect .77   18    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 22   450 220 false(unreach-call) 1 wit inspect 3.5  380 false(unreach-call) 1 wit inspect 17     600   unknown 0 wit inspect 2.1  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect 79   1000 880 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (invalid witness file) 0 wit inspect 3.3   200  
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 8.1 280 58 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 18     990  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 8.4 280 75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 12     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 8.0 270 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 9.3   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 8.0 270 75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  240 true 2 wit inspect 11     250  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 8.0 270 77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 9.7   250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 160   540 1900 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    500 error (7) 0 wit inspect 150     2600  
float-benchs/bary_diverge_true-unreach-call_true-termination.c true 2 wit inspect 84   820 850 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1200 timeout 0 wit inspect 960     2200  
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 7.3 260 59 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 4.4   220  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 2 wit inspect 100   590 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 timeout 0 wit inspect 960     2900  
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c true 2 wit inspect 790   6700 9400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     4600  
float-benchs/divmul_diverge_true-unreach-call_true-termination.c true 2 wit inspect 780   6500 11000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 timeout 0 wit inspect 960     4600  
float-benchs/drift_tenth_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 18   530 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 4.6   220  
float-benchs/exp_loop_true-unreach-call.c unknown 0 wit inspect 680   220 7600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .018 4.9
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   6100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.8
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 31   660 260 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .76 47 error (invalid witness file) 0 wit inspect 4.6   200  
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900   380 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .020 5.0
float-benchs/filter2_iterated_true-unreach-call.c unknown 0 wit inspect 400   540 5100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .019 4.9
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .020 5.0
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 wit inspect 900   540 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 5.0
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   530 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 5.0
float-benchs/filter_iir_true-unreach-call.c unknown 0 wit inspect 810   410 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .023 5.0
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 8.3 270 75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     250  
float-benchs/image_filter_true-unreach-call.c unknown 0 wit inspect 870   2300 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8
float-benchs/interpolation2_true-unreach-call_true-termination.c unknown 0 wit inspect 820   220 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .018 4.9
float-benchs/interpolation_true-unreach-call_true-termination.c timeout 0 wit inspect 900   220 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .018 4.9
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect 13   300 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  280 true 2 wit inspect 130     860  
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 8.7 280 73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 18     320  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 8.6 280 73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 57     360  
float-benchs/loop_true-unreach-call.c true 2 wit inspect 43   600 440 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 timeout 0 wit inspect 960     970  
float-benchs/mea8000_true-unreach-call.c unknown 0 wit inspect 780   670 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect 8.0 270 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect 8.4 270 75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 12     250  
float-benchs/rlim_exit_true-unreach-call_true-termination.c true 2 wit inspect 780   3400 10000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1900 timeout 0 wit inspect 960     4700  
float-benchs/rlim_invariant_true-unreach-call_true-termination.c true 2 wit inspect 22   470 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  310 timeout 0 wit inspect 960     960  
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c timeout 0 wit inspect 900   240 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .020 4.9
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c timeout 0 wit inspect 900   240 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .019 4.9
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c timeout 0 wit inspect 900   250 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 42 error (2) 0 wit inspect .018 4.9
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 0 wit inspect 900   1700 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .021 4.9
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 0 wit inspect 900   900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.9
float-benchs/sqrt_Householder_constant_true-unreach-call.c true 2 wit inspect 200   1400 2500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 error (7) 0 wit inspect 240     3000  
float-benchs/sqrt_Householder_interval_true-unreach-call.c timeout 0 wit inspect 900   230 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.8
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900   440 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .048 4.8
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900   340 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .018 4.8
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900   460 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9
float-benchs/sqrt_poly_true-unreach-call_true-termination.c true 2 wit inspect 49   510 530 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 46    490 true 2 wit inspect 150     1100  
float-benchs/water_pid_true-unreach-call_true-termination.c true 2 wit inspect 56   1100 540 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .43 46 error (invalid witness file) 0 wit inspect 3.0   200  
float-benchs/zonotope_2_true-unreach-call_true-termination.c true 2 wit inspect 210   1800 2300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    810 timeout 0 wit inspect 960     2200  
float-benchs/zonotope_3_true-unreach-call_true-termination.c true 2 wit inspect 23   520 210 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  340 timeout 0 wit inspect 960     5100  
float-benchs/zonotope_loose_true-unreach-call_true-termination.c true 2 wit inspect 11   330 95 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  330 true 2 wit inspect 120     910  
float-benchs/zonotope_tight_true-unreach-call_true-termination.c true 2 wit inspect 11   340 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  310 true 2 wit inspect 110     950  
floats-esbmc-regression/Double_div_true-unreach-call.i true 2 wit inspect 12   340 99 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  320 true 2 wit inspect 230     2700  
floats-esbmc-regression/Float_div_true-unreach-call.i true 2 wit inspect 12   300 88 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  280 true 2 wit inspect 170     570  
floats-esbmc-regression/ceil_nondet_true-unreach-call.i true 2 wit inspect 190   330 2100 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.2  260 unknown 0 wit inspect 7.9   200  
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect 18   290 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 unknown 0 wit inspect 4.0   210  
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect 17   280 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  260 unknown 0 wit inspect 2.6   200  
floats-esbmc-regression/digits_for_true-unreach-call.i true 2 wit inspect 16   270 120 - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 3.3  260 timeout 0 wit inspect 960     3200  
floats-esbmc-regression/digits_while_true-unreach-call.i true 2 wit inspect 16   270 150 - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 4.0  260 timeout 0 wit inspect 960     2900  
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect 17   280 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 true 2 wit inspect 13     280  
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect 17   280 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 unknown 0 wit inspect 3.9   200  
floats-esbmc-regression/floor_nondet_true-unreach-call.i true 2 wit inspect 190   320 2300 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.5  250 unknown 0 wit inspect 8.7   210  
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect 18   280 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 unknown 0 wit inspect 4.6   200  
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect 18   280 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  260 true 2 wit inspect 6.3   260  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect 17   290 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 11     280  
floats-esbmc-regression/fmod2_true-unreach-call.i true 2 wit inspect 22   530 190 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8  470 unknown 0 wit inspect 6.5   210  
floats-esbmc-regression/fmod3_true-unreach-call.i true 2 wit inspect 22   520 190 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.3  470 unknown 0 wit inspect 8.0   200  
floats-esbmc-regression/fmod_true-unreach-call.i true 2 wit inspect 18   280 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  250 unknown 0 wit inspect 3.9   200  
floats-esbmc-regression/isgreater_true-unreach-call.i true 2 wit inspect 15   280 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 8.8   270  
floats-esbmc-regression/isgreaterequal_true-unreach-call.i true 2 wit inspect 15   280 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 9.3   270  
floats-esbmc-regression/isless_true-unreach-call.i true 2 wit inspect 15   280 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 9.1   260  
floats-esbmc-regression/islessequal_true-unreach-call.i true 2 wit inspect 15   290 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  260 true 2 wit inspect 8.9   260  
floats-esbmc-regression/islessgreater_true-unreach-call.i true 2 wit inspect 15   290 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 9.3   280  
floats-esbmc-regression/isunordered_true-unreach-call.i true 2 wit inspect 16   310 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 true 2 wit inspect 9.3   270  
floats-esbmc-regression/lrint_true-unreach-call.i true 2 wit inspect 19   370 150 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.4  270 unknown 0 wit inspect 3.4   200  
floats-esbmc-regression/modf_true-unreach-call.i true 2 wit inspect 18   280 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 unknown 0 wit inspect 3.8   210  
floats-esbmc-regression/nan_true-unreach-call.i true 2 wit inspect 18   290 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 10     290  
floats-esbmc-regression/nearbyint2_true-unreach-call.i true 2 wit inspect 19   380 170 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.1  260 unknown 0 wit inspect 3.9   200  
floats-esbmc-regression/nearbyint_true-unreach-call.i true 2 wit inspect 260   230 2900 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.6  270 unknown 0 wit inspect 5.7   200  
floats-esbmc-regression/remainder_true-unreach-call.i error 0 wit inspect 2.3 140 20 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .018 4.8
floats-esbmc-regression/rint2_true-unreach-call.i true 2 wit inspect 19   390 160 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.0  270 unknown 0 wit inspect 4.1   210  
floats-esbmc-regression/rint_true-unreach-call.i true 2 wit inspect 260   240 3000 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.5  270 unknown 0 wit inspect 4.3   210  
floats-esbmc-regression/round_nondet_true-unreach-call.i true 2 wit inspect 190   350 2300 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.3  260 unknown 0 wit inspect 7.7   210  
floats-esbmc-regression/round_true-unreach-call.i true 2 wit inspect 19   290 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  260 unknown 0 wit inspect 3.8   200  
floats-esbmc-regression/rounding_functions_true-unreach-call.i true 2 wit inspect 19   290 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  260 unknown 0 wit inspect 4.0   210  
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i true 2 wit inspect 180   310 2200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  270 unknown 0 wit inspect 7.8   210  
floats-esbmc-regression/trunc_nondet_true-unreach-call.i true 2 wit inspect 180   340 2600 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.4  250 unknown 0 wit inspect 7.4   200  
floats-esbmc-regression/trunc_true-unreach-call.i true 2 wit inspect 18   300 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 unknown 0 wit inspect 5.3   270  
floats-esbmc-regression/Double_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect 250   3600 2700 true -32 wit inspect 11    900 timeout 0 wit inspect 95     7000   unknown 0 wit inspect 5.4  520 false(unreach-call) 1 wit inspect 1.5    36    - wit inspect - wit inspect
floats-esbmc-regression/Float_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect 230   1000 2900 true -32 wit inspect 4.1  290 timeout 0 wit inspect 96     3500   unknown 0 wit inspect 3.1  230 false(unreach-call) 1 wit inspect .73   21    - wit inspect - wit inspect
floats-esbmc-regression/digits_bad_for_false-unreach-call.i false(unreach-call) 0 wit inspect 15   220 120 assertion 0 wit inspect 3.9  270 out of memory 0 wit inspect 67     7000   unknown 0 wit inspect 2.6  210 true -32 wit inspect .71   19    - wit inspect - wit inspect
floats-esbmc-regression/digits_bad_while_false-unreach-call.i false(unreach-call) 0 wit inspect 15   220 140 assertion 0 wit inspect 3.9  270 timeout 0 wit inspect 96     1700   unknown 0 wit inspect 2.4  220 true -32 wit inspect .64   19    - wit inspect - wit inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 172 202 50000 89000 630000 31 -77 360 8300 31 15 1100 29000 31 0 68 5500 31 -636 16   460 141 128 10000   43000 141 112 16000 73000
    correct results 120 218 9200 65000 110000 19 19 330 6000 15 15 310 7500 0 4 4 3.4 94 72 144 1300   21000 56 112 2300 24000
        correct true 98 196 7600 53000 91000 0 0 0 0 72 144 1300   21000 56 112 2300 24000
        correct false 22 22 1600 12000 16000 19 19 330 6000 15 15 310 7500 0 4 4 3.4 94 0 0
    correct-unconfimed results 2 0 31 440 260 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 2 0 31 440 260 0 0 0 0 0 0
    incorrect results 1 -16 18 530 150 3 -96 17 1400 0 0 20 -640 12   370 1 -16 6.4 280 0
        incorrect true 0 3 -96 17 1400 0 0 20 -640 12   370 0 0
        incorrect false 1 -16 18 530 150 0 0 0 0 1 -16 6.4 280 0
score (172 tasks, max score: 313) 202 -77 15 0 -636 128 112
Run set veriabs.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Floats