Tool CBMC 5.8 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*
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-11-30 11:20:26 CET 2017-12-01 07:26:01 CET 2017-12-01 07:56:00 CET 2017-12-01 08:08:00 CET 2017-12-01 08:15:34 CET 2017-12-01 04:22:29 CET 2017-12-01 07:31:28 CET
Run set cbmc.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Floats
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cbmc.2017-11-30_1120.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 3.1  59 31   false(unreach-call) 1 wit inspect 4.9  360 false(unreach-call) 1 wit inspect 54     690   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.9  58 28   false(unreach-call) 1 wit inspect 4.2  350 timeout 0 wit inspect 97     680   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.9  61 54   false(unreach-call) 1 wit inspect 4.6  360 false(unreach-call) 1 wit inspect 23     670   unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.5  60 29   false(unreach-call) 1 wit inspect 4.6  360 false(unreach-call) 1 wit inspect 46     670   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.5  60 37   false(unreach-call) 1 wit inspect 4.7  360 false(unreach-call) 1 wit inspect 34     670   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .72   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 22    130 190   true -32 wit inspect 3.7  260 timeout 0 wit inspect 97     820   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 28    140 260   true -32 wit inspect 3.3  260 timeout 0 wit inspect 97     830   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.7  91 36   true -32 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 29     810   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 50    220 600   true -32 wit inspect 4.0  250 timeout 0 wit inspect 97     890   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 43    220 420   true -32 wit inspect 3.2  260 timeout 0 wit inspect 97     880   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 29    180 260   true -32 wit inspect 3.3  260 timeout 0 wit inspect 97     920   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.3  43 17   true -32 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 21     570   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .75 42 8.1 true -32 wit inspect 3.0  270 false(unreach-call) 1 wit inspect 28     570   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.8  49 22   false(unreach-call) 1 wit inspect 3.8  300 timeout 0 wit inspect 97     600   unknown 0 wit inspect 3.4  180 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.0  42 14   false(unreach-call) 1 wit inspect 4.5  320 timeout 0 wit inspect 97     440   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.2  43 15   true -32 wit inspect 3.6  260 timeout 0 wit inspect 97     410   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 1.2  42 17   true -32 wit inspect 3.7  260 timeout 0 wit inspect 97     440   unknown 0 wit inspect 3.0  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i true 2 wit inspect 18    65 180   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 2 wit inspect 14    72 200   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    600 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 2 wit inspect 22    66 240   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    620 timeout 0 wit inspect 960     950  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i true 2 wit inspect 48    130 470   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    530 timeout 0 wit inspect 960     990  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i true 2 wit inspect 55    140 600   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    840 timeout 0 wit inspect 960     980  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 2 wit inspect 68    150 740   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    530 timeout 0 wit inspect 960     940  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i true 2 wit inspect 47    130 700   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    580 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i true 2 wit inspect 75    140 790   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i true 2 wit inspect 120    190 1000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    600 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i true 2 wit inspect 140    220 1400   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    560 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i true 2 wit inspect 160    220 1500   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    690 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i true 2 wit inspect 120    220 1000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    730 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i true 2 wit inspect 110    220 1400   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     1100  
floats-cdfpl/sine_4_true-unreach-call_true-termination.i true 2 wit inspect 69    55 870   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    500 timeout 0 wit inspect 960     850  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i true 2 wit inspect 5.6  48 69   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    490 timeout 0 wit inspect 960     830  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 2 wit inspect 3.2  44 41   - 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 3.5  49 40   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 740    590 timeout 0 wit inspect 960     760  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 3.0  46 34   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 540    540 timeout 0 wit inspect 960     830  
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 140    63 2100   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 660    560 true 2 wit inspect 780     830  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 120    63 1500   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 510    510 true 2 wit inspect 490     740  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 13    49 140   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 260    500 true 2 wit inspect 350     810  
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 17    50 190   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 890    480 true 2 wit inspect 180     700  
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 1.6  43 19   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 61    360 true 2 wit inspect 120     610  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 1.2  43 11   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  320 true 2 wit inspect 33     610  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 1.3  47 13   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    790 true 2 wit inspect 31     690  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect .40 33 3.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 8.9   230  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 3.0  39 34   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    300 true 2 wit inspect 43     390  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect .41 33 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 8.8   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 1.1  39 9.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 37     550  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect .39 33 4.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect .43 33 3.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  240 true 2 wit inspect 9.4   240  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .90 37 8.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 9.9   290  
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect .90 39 8.4 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.9  260 unknown 0 wit inspect 4.0   200  
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect .95 37 10   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 260     520  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect .39 33 3.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 9.2   250  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect .38 33 5.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 11     290  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect .40 33 3.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.6   240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect .43 33 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 15     270  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect .44 33 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 11     270  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect .90 37 7.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 2.6  38 27   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.8  290 unknown 0 wit inspect 3.8   210  
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect .91 37 9.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 7.9   290  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect .39 33 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     300  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect .42 35 5.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 16     390  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 1.1  39 12   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  300 true 2 wit inspect 83     590  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect .44 33 4.0 - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 4.9  280 true 2 wit inspect 300     1100  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect .40 33 4.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  250 true 2 wit inspect 10     280  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect .44 33 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 true 2 wit inspect 13     340  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 14    49 170   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 81    330 true 2 wit inspect 71     450  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect .42 33 4.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 27     270  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect .43 33 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 12     290  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 1.4  37 14   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.5  260 true 2 wit inspect 11     290  
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect 1.1  39 9.5 - wit inspect - wit inspect - wit inspect - wit inspect error (parsing failed) 0 wit inspect 2.2  140 error (7) 0 wit inspect 11     260  
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 1.0  38 11   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 16     560  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .25 33 2.3 true -32 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 13     280   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .26 33 2.7 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 12     270   unknown 0 wit inspect 4.0  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .29 34 2.2 false(unreach-call) 1 wit inspect 4.5  270 false(unreach-call) 1 wit inspect 10     280   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .75   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .28 34 2.4 false(unreach-call) 1 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 14     290   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c error (42) 0 wit inspect 870    250 6800   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .26 35 2.2 false(unreach-call) 1 wit inspect 3.1  270 false(unreach-call) 1 wit inspect 12     300   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .23 33 2.2 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.0   230   unknown 0 wit inspect 2.6  180 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .25 33 2.2 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.3   220   unknown 0 wit inspect 2.7  180 error (2) 0 wit inspect .56   18    - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.7  240 30   false(unreach-call) 1 wit inspect 5.0  360 timeout 0 wit inspect 97     1200   unknown 0 wit inspect 4.0  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect .72 50 7.5 true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 21     610   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect 3.0  33 36   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 13    510 timeout 0 wit inspect 960     3400  
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect .41 33 3.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 21     970  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect .43 33 3.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 14     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect .39 33 4.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 9.9   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect .40 33 5.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.9   250  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect .41 33 4.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 11     250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 94    240 940   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    500 error (7) 0 wit inspect 37     1000  
float-benchs/bary_diverge_true-unreach-call_true-termination.c error (42) 0 wit inspect 870    1200 9100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .024 4.9
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect .44 33 3.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 4.4   230  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 2 wit inspect 11    110 94   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1400 timeout 0 wit inspect 960     2900  
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c error (42) 0 wit inspect 870    3200 5700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8
float-benchs/divmul_diverge_true-unreach-call_true-termination.c error (42) 0 wit inspect 870    3100 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .019 4.9
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 1.2  33 10   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.5  270 error (7) 0 wit inspect 370     590  
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 3.4  42 39   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 8.1  350 timeout 0 wit inspect 960     1300  
float-benchs/feedback_diverge_true-unreach-call_true-termination.c error (42) 0 wit inspect 870    1100 8500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .026 4.8
float-benchs/filter1_true-unreach-call_true-termination.c error (42) 0 wit inspect 870    1600 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 46 error (2) 0 wit inspect .018 4.9
float-benchs/filter2_alt_true-unreach-call.c error (42) 0 wit inspect 870    180 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.9
float-benchs/filter2_iterated_true-unreach-call.c error (42) 0 wit inspect 870    1300 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.9
float-benchs/filter2_reinit_true-unreach-call_true-termination.c error (42) 0 wit inspect 870    490 8400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 45 error (2) 0 wit inspect .021 4.9
float-benchs/filter2_set_true-unreach-call_true-termination.c error (42) 0 wit inspect 870    450 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.9
float-benchs/filter2_true-unreach-call_true-termination.c error (42) 0 wit inspect 870    480 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.8
float-benchs/filter_iir_true-unreach-call.c error (42) 0 wit inspect 870    750 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .020 4.9
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect .44 33 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.6   260  
float-benchs/image_filter_true-unreach-call.c true 2 wit inspect 850    2800 6000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 75     7000  
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect 1.2  36 13   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 timeout 0 wit inspect 960     740  
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect 1.1  36 11   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     850  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect .71 36 6.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  280 error (7) 0 wit inspect 41     580  
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect .46 35 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 15     310  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect .48 35 4.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 59     350  
float-benchs/loop_true-unreach-call.c out of memory 0 wit inspect 480    15000 6200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .042 4.8
float-benchs/mea8000_true-unreach-call.c error (134) 0 wit inspect 230    13000 2500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .027 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect .42 33 3.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.7   250  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect .43 33 4.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 11     240  
float-benchs/rlim_exit_true-unreach-call_true-termination.c error (134) 0 wit inspect 180    14000 2600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .020 4.9
float-benchs/rlim_invariant_true-unreach-call_true-termination.c error (42) 0 wit inspect 870    1300 7900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c error (1) 0 wit inspect 870    310 8900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 4.9
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c error (1) 0 wit inspect 870    300 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .019 4.9
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c error (1) 0 wit inspect 870    290 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .017 4.8
float-benchs/sin_interpolated_negation_true-unreach-call.c error (42) 0 wit inspect 870    4300 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .020 4.9
float-benchs/sin_interpolated_smallrange_true-unreach-call.c error (42) 0 wit inspect 870    3000 6200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .041 4.9
float-benchs/sqrt_Householder_constant_true-unreach-call.c true 2 wit inspect 3.4  33 36   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 61    1200 error (7) 0 wit inspect 280     3000  
float-benchs/sqrt_Householder_interval_true-unreach-call.c error (42) 0 wit inspect 870    590 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .020 4.8
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c error (42) 0 wit inspect 870    3000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .022 4.8
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c error (42) 0 wit inspect 870    2000 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .022 4.8
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c error (42) 0 wit inspect 870    3300 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.9
float-benchs/sqrt_poly_true-unreach-call_true-termination.c true 2 wit inspect 3.5  64 38   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 37    490 true 2 wit inspect 150     1100  
float-benchs/water_pid_true-unreach-call_true-termination.c true 2 wit inspect 3.8  36 39   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 26    780 error (7) 0 wit inspect 180     2900  
float-benchs/zonotope_2_true-unreach-call_true-termination.c true 2 wit inspect 400    5500 4100   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960    5500 timeout 0 wit inspect 960     4700  
float-benchs/zonotope_3_true-unreach-call_true-termination.c error (134) 0 wit inspect 230    15000 3300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .023 4.9
float-benchs/zonotope_loose_true-unreach-call_true-termination.c true 2 wit inspect .65 40 6.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  310 true 2 wit inspect 120     930  
float-benchs/zonotope_tight_true-unreach-call_true-termination.c true 2 wit inspect .67 40 7.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  310 true 2 wit inspect 170     1000  
floats-esbmc-regression/Double_div_true-unreach-call.i true 2 wit inspect 5.6  34 66   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 12    500 true 2 wit inspect 270     2700  
floats-esbmc-regression/Float_div_true-unreach-call.i true 2 wit inspect 2.8  33 27   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 7.4  300 true 2 wit inspect 120     540  
floats-esbmc-regression/ceil_nondet_true-unreach-call.i true 2 wit inspect 6.9  57 81   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.1  260 unknown 0 wit inspect 8.0   210  
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect 1.9  39 20   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 unknown 0 wit inspect 3.7   210  
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect 1.4  38 11   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 unknown 0 wit inspect 3.9   210  
floats-esbmc-regression/digits_for_true-unreach-call.i true 2 wit inspect 2.9  33 30   - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 5.6  280 timeout 0 wit inspect 960     3200  
floats-esbmc-regression/digits_while_true-unreach-call.i true 2 wit inspect 2.9  33 29   - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 4.4  260 timeout 0 wit inspect 960     2900  
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect .90 37 8.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  250 true 2 wit inspect 10     280  
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect 1.0  39 11   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 unknown 0 wit inspect 4.0   200  
floats-esbmc-regression/floor_nondet_true-unreach-call.i true 2 wit inspect 7.1  59 74   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.2  250 unknown 0 wit inspect 7.6   210  
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect 1.9  39 22   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 unknown 0 wit inspect 3.8   210  
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect 1.4  38 15   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  250 true 2 wit inspect 9.2   270  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect 1.4  38 12   - wit inspect - wit inspect - wit inspect - wit inspect