Tool CPAchecker 1.6.1-svn 26758M 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] 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:36:48 CET 2017-12-01 08:27:40 CET 2017-12-01 08:32:13 CET 2017-12-01 08:39:14 CET 2017-12-01 04:24:39 CET 2017-12-01 07:43:13 CET
Run set cpa-bam-slicing.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Floats
Options -ldv-bam-svcomp -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-slicing.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) 0 wit inspect 33   390 240 true -32 wit inspect 3.6  260 true -32 wit inspect 4.7   220   unknown 0 wit inspect 2.7  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 49   390 350 true -32 wit inspect 3.3  260 true -32 wit inspect 4.4   210   unknown 0 wit inspect 2.8  190 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 12   390 120 true -32 wit inspect 3.1  250 true -32 wit inspect 4.4   230   unknown 0 wit inspect 2.9  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 12   390 98 true -32 wit inspect 3.4  250 true -32 wit inspect 4.5   230   unknown 0 wit inspect 2.9  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 13   380 110 true -32 wit inspect 4.0  260 true -32 wit inspect 3.0   220   unknown 0 wit inspect 2.8  180 true -32 wit inspect .62   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 40   490 350 true -32 wit inspect 3.4  260 true -32 wit inspect 5.1   230   unknown 0 wit inspect 2.9  180 true -32 wit inspect .61   19    - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 40   490 340 true -32 wit inspect 3.3  250 true -32 wit inspect 4.5   230   unknown 0 wit inspect 2.7  180 true -32 wit inspect .61   19    - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 14   480 140 true -32 wit inspect 3.4  260 true -32 wit inspect 4.4   220   unknown 0 wit inspect 2.9  180 true -32 wit inspect .67   19    - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 120   600 1100 true -32 wit inspect 3.3  260 true -32 wit inspect 4.5   230   unknown 0 wit inspect 2.9  180 true -32 wit inspect .60   19    - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 43   590 300 true -32 wit inspect 3.4  250 true -32 wit inspect 3.1   230   unknown 0 wit inspect 2.8  180 true -32 wit inspect .61   19    - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 18   590 150 true -32 wit inspect 3.5  280 true -32 wit inspect 4.4   220   unknown 0 wit inspect 2.1  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 24   360 190 true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 22     560   unknown 0 wit inspect 2.7  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.0 350 36 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 27     570   unknown 0 wit inspect 2.9  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 480   570 3900 true -32 wit inspect 4.0  250 timeout 0 wit inspect 97     620   unknown 0 wit inspect 1.9  190 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 12   360 110 true -32 wit inspect 4.1  270 timeout 0 wit inspect 97     440   unknown 0 wit inspect 2.8  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 170   490 1400 true -32 wit inspect 3.5  250 false(unreach-call) 1 wit inspect 87     430   unknown 0 wit inspect 2.9  190 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 46   400 400 true -32 wit inspect 3.3  270 timeout 0 wit inspect 97     450   unknown 0 wit inspect 2.7  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   620 6500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .024 4.8
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820 6100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   760 6300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   700 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 5.0
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   640 8200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .021 4.8
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   750 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .024 5.0
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   630 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.8
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   630 6300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .024 4.9
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   630 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   720 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .022 4.8
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   720 6500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 4.8
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820 6500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   680 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .020 5.0
floats-cdfpl/sine_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   590 8500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .024 4.8
floats-cdfpl/sine_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   540 5900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .024 4.8
floats-cdfpl/sine_6_true-unreach-call_true-termination.i unknown 0 wit inspect 290   490 2900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.8
floats-cdfpl/sine_7_true-unreach-call_true-termination.i unknown 0 wit inspect 750   600 5400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .019 4.9
floats-cdfpl/sine_8_true-unreach-call_true-termination.i timeout 0 wit inspect 900   560 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 4.8
floats-cdfpl/square_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   680 6500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/square_5_true-unreach-call_true-termination.i unknown 0 wit inspect 660   630 5000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .025 4.8
floats-cdfpl/square_6_true-unreach-call_true-termination.i unknown 0 wit inspect 310   540 2500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8
floats-cdfpl/square_7_true-unreach-call_true-termination.i unknown 0 wit inspect 400   490 2800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .020 4.9
floats-cdfpl/square_8_true-unreach-call_true-termination.i unknown 0 wit inspect 9.5 350 85 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float-div1_true-unreach-call.i unknown 0 wit inspect 3.6 320 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 5.0
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i assertion 0 wit inspect 1.8 130 18 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .022 4.9
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 2.7 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.2   250  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 3.1 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    300 true 2 wit inspect 42     390  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 9.7   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i unknown 0 wit inspect 3.6 290 34 - 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
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 13     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 14     290  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.3  250 unknown 0 wit inspect 3.9   210  
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 170     450  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  260 true 2 wit inspect 12     240  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 12     280  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 16     240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 true 2 wit inspect 16     270  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     250  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  250 true 2 wit inspect 9.6   290  
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 3.1 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    420 unknown 0 wit inspect 3.7   210  
floats-cbmc-regression/float19_true-unreach-call.i unknown 0 wit inspect 3.0 280 27 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 9.2   230  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 19     410  
floats-cbmc-regression/float21_true-unreach-call.i unknown 0 wit inspect 3.2 280 26 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .025 4.9
floats-cbmc-regression/float22_true-unreach-call_true-termination.i unknown 0 wit inspect 3.0 290 28 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .025 4.8
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 2.7 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     280  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  270 true 2 wit inspect 17     330  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 3.2 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 71    330 true 2 wit inspect 77     440  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 26     280  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 3.0 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 12     280  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8  270 true 2 wit inspect 14     290  
floats-cbmc-regression/float_lib1_true-unreach-call.i assertion 0 wit inspect 1.6 130 14 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 3.2 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 20     530  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 280 32 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 11     280   unknown 0 wit inspect 2.8  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 3.6 300 32 true -32 wit inspect 3.1  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 2.8  210 true -32 wit inspect .62   19    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 3.2 290 29 true -32 wit inspect 4.1  250 true -32 wit inspect 5.1   230   unknown 0 wit inspect 2.9  180 true -32 wit inspect .74   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 300 27 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 9.6   300   unknown 0 wit inspect 2.8  180 true -32 wit inspect .62   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c unknown 0 wit inspect 4.3 370 41 error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 300 33 true -32 wit inspect 3.2  250 false(unreach-call) 1 wit inspect 9.8   270   unknown 0 wit inspect 3.0  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c true -32 wit inspect 2.8 270 24 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 3.0   220   unknown 0 wit inspect .95 51 error (1) 0 wit inspect .069  9.0  - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c true -32 wit inspect 2.7 270 24 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 4.8   220   unknown 0 wit inspect .92 51 error (1) 0 wit inspect .074  9.0  - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c unknown 0 wit inspect 3.3 280 30 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .88 51 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 6.3 470 58 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 20     620   unknown 0 wit inspect 3.0  210 true -32 wit inspect .62   19    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c out of memory 0 wit inspect 630   15000 8500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.9
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 28     980  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 15     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.7 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 10     270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  270 true 2 wit inspect 9.3   250  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 10     250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c unknown 0 wit inspect 8.0 460 65 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .021 4.9
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1800 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .025 4.8
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 2.7 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 5.3   240  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c unknown 0 wit inspect 330   830 1800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 4.8
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .019 4.9
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 4.0 280 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    310 true 2 wit inspect 290     590  
float-benchs/exp_loop_true-unreach-call.c unknown 0 wit inspect 4.0 330 41 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .023 4.9
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .024 4.9
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 3.5 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.2  400 true 2 wit inspect 460     880  
float-benchs/filter2_alt_true-unreach-call.c unknown 0 wit inspect 6.1 340 71 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .022 4.8
float-benchs/filter2_iterated_true-unreach-call.c unknown 0 wit inspect 6.1 510 59 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.8
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .023 4.8
float-benchs/filter2_set_true-unreach-call_true-termination.c unknown 0 wit inspect 8.6 470 84 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .024 4.8
float-benchs/filter2_true-unreach-call_true-termination.c true 2 wit inspect 35   1400 290 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 timeout 0 wit inspect 960     2000  
float-benchs/filter_iir_true-unreach-call.c true 2 wit inspect 3.3 280 30 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 timeout 0 wit inspect 960     1400  
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 2.7 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 11     250  
float-benchs/image_filter_true-unreach-call.c timeout 0 wit inspect 900   4700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
float-benchs/interpolation2_true-unreach-call_true-termination.c unknown 0 wit inspect 6.3 340 68 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .019 4.8
float-benchs/interpolation_true-unreach-call_true-termination.c unknown 0 wit inspect 8.2 330 92 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.9
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.6 310 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 150     830  
float-benchs/inv_square_int_true-unreach-call_true-termination.c unknown 0 wit inspect 3.1 290 30 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .024 5.0
float-benchs/inv_square_true-unreach-call_true-termination.c unknown 0 wit inspect 3.1 300 30 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .020 4.9
float-benchs/loop_true-unreach-call.c timeout 0 wit inspect 900   4400 7300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 45 error (2) 0 wit inspect .026 4.8
float-benchs/mea8000_true-unreach-call.c timeout 0 wit inspect 900   4100 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .023 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 11     240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 11     260  
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.9
float-benchs/rlim_invariant_true-unreach-call_true-termination.c true 2 wit inspect 3.7 280 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  310 timeout 0 wit inspect 960     790  
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c error 0 wit inspect 2.7 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 45 error (2) 0 wit inspect .025 4.8
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c error 0 wit inspect 2.6 270 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .024 4.8
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c unknown 0 wit inspect 3.2 280 29 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .024 4.8
float-benchs/sin_interpolated_negation_true-unreach-call.c error 0 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .020 4.9
float-benchs/sin_interpolated_smallrange_true-unreach-call.c error 0 wit inspect 2.7 260 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 45 error (2) 0 wit inspect .019 4.9
float-benchs/sqrt_Householder_constant_true-unreach-call.c true 2 wit inspect 7.5 440 58 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3100 error (7) 0 wit inspect 260     3000  
float-benchs/sqrt_Householder_interval_true-unreach-call.c unknown 0 wit inspect 6.0 520 50 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 4.9
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c unknown 0 wit inspect 5.5 540 53 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.8
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c unknown 0 wit inspect 5.6 540 58 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .020 4.9
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c unknown 0 wit inspect 5.5 540 54 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8
float-benchs/sqrt_poly_true-unreach-call_true-termination.c unknown 0 wit inspect 35   490 300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9
float-benchs/water_pid_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1300 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.9
float-benchs/zonotope_2_true-unreach-call_true-termination.c true 2 wit inspect 3.8 270 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    880 timeout 0 wit inspect 960     2500  
float-benchs/zonotope_3_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4100 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .024 5.0
float-benchs/zonotope_loose_true-unreach-call_true-termination.c unknown 0 wit inspect 3.6 340 40 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .021 4.8
float-benchs/zonotope_tight_true-unreach-call_true-termination.c unknown 0 wit inspect 3.9 340 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .024 4.9
floats-esbmc-regression/Double_div_true-unreach-call.i timeout 0 wit inspect 900   4100 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .018 4.8
floats-esbmc-regression/Float_div_true-unreach-call.i timeout 0 wit inspect 900   4100 9100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 5.0
floats-esbmc-regression/ceil_nondet_true-unreach-call.i false(unreach-call) -16 wit inspect 3.6 290 35 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.1  260 unknown 0 wit inspect 7.7   210  
floats-esbmc-regression/ceil_true-unreach-call.i false(unreach-call) -16 wit inspect 3.6 300 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 unknown 0 wit inspect 4.7   210  
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect 3.5 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  250 unknown 0 wit inspect 3.9   200  
floats-esbmc-regression/digits_for_true-unreach-call.i assertion 0 wit inspect 1.5 130 12 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/digits_while_true-unreach-call.i assertion 0 wit inspect 1.5 130 15 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect 3.3 270 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 11     270  
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect 3.0 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 unknown 0 wit inspect 3.7   210  
floats-esbmc-regression/floor_nondet_true-unreach-call.i false(unreach-call) -16 wit inspect 3.7 290 32 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.9  260 unknown 0 wit inspect 7.7   210  
floats-esbmc-regression/floor_true-unreach-call.i false(unreach-call) -16 wit inspect 3.4 290 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 unknown 0 wit inspect 3.9   210  
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 11     270  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit