Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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* [apollon005; apollon043; apollon077; apollon078; apollon087; apollon118] [apollon061; apollon077; apollon078; apollon086; apollon134] [apollon038; apollon077; apollon078; apollon083] [apollon077; apollon078; apollon161] 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: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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-01 22:41:19 CET 2017-12-02 21:10:50 CET 2017-12-02 22:39:24 CET 2017-12-02 22:51:52 CET 2017-12-02 23:01:21 CET 2017-12-02 19:44:15 CET 2017-12-02 21:36:25 CET
Run set symbiotic.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Floats
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.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 unknown 0 wit inspect .16  11 1.9  error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.9  error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .046 4.9 error (invalid witness file) 0 wit inspect .68 50 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i unknown 0 wit inspect .16  11 2.0  error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0037 .29 - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.8  error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .89 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i unknown 0 wit inspect .16  11 2.0  error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0033 .28 - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i unknown 0 wit inspect .19  11 2.1  error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9 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_7_false-unreach-call_true-termination.i unknown 0 wit inspect .16  11 1.8  error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i unknown 0 wit inspect .16  11 1.8  error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0033 .26 - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.9  error (invalid witness file) 0 wit inspect .50 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0034 .26 - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.7  error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0025 .26 - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i unknown 0 wit inspect .17  11 1.9  error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0030 .28 - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i unknown 0 wit inspect .19  11 1.8  error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i unknown 0 wit inspect .16  11 2.0  error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i unknown 0 wit inspect .16  11 2.0  error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 51 error (invalid witness file) 0 wit inspect .0032 .29 - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.6  error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0010 .29 - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i unknown 0 wit inspect .16  11 1.5  error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i unknown 0 wit inspect .18  11 2.0  error (invalid witness file) 0 wit inspect .41 45 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i unknown 0 wit inspect .19  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.8
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .025 4.9
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.7  - 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
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i unknown 0 wit inspect .18  11 2.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i unknown 0 wit inspect .19  11 1.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .027 5.0
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i unknown 0 wit inspect .19  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 5.0
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i unknown 0 wit inspect .17  11 2.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .020 4.9
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i unknown 0 wit inspect .16  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i unknown 0 wit inspect .18  11 2.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .021 4.9
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i unknown 0 wit inspect .19  11 1.8  - 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
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i unknown 0 wit inspect .16  11 1.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .020 4.9
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i unknown 0 wit inspect .18  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 5.0
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.8
floats-cdfpl/sine_4_true-unreach-call_true-termination.i unknown 0 wit inspect .16  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.9
floats-cdfpl/sine_5_true-unreach-call_true-termination.i unknown 0 wit inspect .16  11 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .019 4.9
floats-cdfpl/sine_6_true-unreach-call_true-termination.i unknown 0 wit inspect .19  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/sine_7_true-unreach-call_true-termination.i unknown 0 wit inspect .16  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/sine_8_true-unreach-call_true-termination.i unknown 0 wit inspect .16  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .021 4.9
floats-cdfpl/square_4_true-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.9
floats-cdfpl/square_5_true-unreach-call_true-termination.i unknown 0 wit inspect .16  11 1.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.8
floats-cdfpl/square_6_true-unreach-call_true-termination.i unknown 0 wit inspect .16  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .020 4.8
floats-cdfpl/square_7_true-unreach-call_true-termination.i unknown 0 wit inspect .16  11 1.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .020 4.9
floats-cdfpl/square_8_true-unreach-call_true-termination.i unknown 0 wit inspect .17  11 2.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float-div1_true-unreach-call.i error 0 wit inspect .17  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .022 5.0
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i error 0 wit inspect .18  12 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 4.8
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect .12  11 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.9   260  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i error 0 wit inspect .17  11 1.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .023 4.8
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect .14  11 1.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 8.4   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i error 0 wit inspect .20  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .024 4.8
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect .15  11 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect .14  11 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 10     240  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .19  11 2.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 wit inspect .13  11 1.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .018 5.0
floats-cbmc-regression/float-to-double1_true-unreach-call.i error 0 wit inspect .17  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect .14  10 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.2   250  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect .15  11 1.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 11     290  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect .12  11 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.5  250 true 2 wit inspect 10     240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .027 4.8
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect .12  11 1.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 11     240  
floats-cbmc-regression/float14_true-unreach-call.i error 0 wit inspect .19  11 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .020 4.9
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect .18  11 2.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    410 unknown 0 wit inspect 4.5   200  
floats-cbmc-regression/float19_true-unreach-call.i error 0 wit inspect .18  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .022 4.9
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect .12  11 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 10     230  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i unknown 0 wit inspect .19  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .018 4.8
floats-cbmc-regression/float21_true-unreach-call.i error 0 wit inspect .18  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .44 44 error (2) 0 wit inspect .020 4.9
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect .15  11 1.4  - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 4.6  280 true 2 wit inspect 340     1100  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect .15  11 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 11     260  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i unknown 0 wit inspect .18  11 1.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float4_true-unreach-call.i error 0 wit inspect .17  11 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .020 4.9
floats-cbmc-regression/float5_true-unreach-call_true-termination.i unknown 0 wit inspect .17  11 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .020 4.8
floats-cbmc-regression/float6_true-unreach-call_true-termination.i unknown 0 wit inspect .16  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float8_true-unreach-call.i error 0 wit inspect .17  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9
floats-cbmc-regression/float_lib1_true-unreach-call.i error 0 wit inspect .18  11 1.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .018 5.0
floats-cbmc-regression/float_lib2_true-unreach-call.i error 0 wit inspect .16  11 2.2  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.8
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15  11 1.6  false(unreach-call) 1 wit inspect 3.2  260 true -32 wit inspect 3.6   240   unknown 0 wit inspect 2.0  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .18  11 1.8  false(unreach-call) 1 wit inspect 3.4  270 true -32 wit inspect 4.7   230   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c unknown 0 wit inspect .15  11 1.8  error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .20  14 1.8  false(unreach-call) 1 wit inspect 3.0  250 true -32 wit inspect 4.2   210   unknown 0 wit inspect 2.7  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 .17  11 2.2  error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c unknown 0 wit inspect .16  11 2.0  error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .18  11 1.6  false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 4.4   210   unknown 0 wit inspect 1.9  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15  11 1.7  false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 3.1   220   unknown 0 wit inspect 2.7  190 true -32 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c unknown 0 wit inspect .20  11 1.9  error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c unknown 0 wit inspect .16  11 1.9  error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0031 .26 - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect .16  11 1.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 timeout 0 wit inspect 960     3400  
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect .14  11 1.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 23     990  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect .14  11 1.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 12     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect .16  11 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 9.7   280  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect .14  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 9.2   260  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect .14  11 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.1  250 true 2 wit inspect 9.2   250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c unknown 0 wit inspect .17  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .024 4.8
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900     69 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .025 4.8
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect .15  11 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.1   230  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c unknown 0 wit inspect .19  11 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.9
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900     1800 8000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.9
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900     1800 8500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .019 4.9
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect .14  11 1.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    310 true 2 wit inspect 380     630  
float-benchs/exp_loop_true-unreach-call.c unknown 0 wit inspect .20  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .019 5.0
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900     1800 8700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 46 error (2) 0 wit inspect .019 5.0
float-benchs/filter1_true-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900     2000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.8
float-benchs/filter2_alt_true-unreach-call.c timeout (timeout) 0 wit inspect 900     70 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .023 4.9
float-benchs/filter2_iterated_true-unreach-call.c timeout (timeout) 0 wit inspect 900     9600 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .024 4.8
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900     69 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.8
float-benchs/filter2_set_true-unreach-call_true-termination.c unknown 0 wit inspect .18  12 2.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 45 error (2) 0 wit inspect .018 4.9
float-benchs/filter2_true-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900     68 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9
float-benchs/filter_iir_true-unreach-call.c timeout (timeout) 0 wit inspect 900     64 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 43 error (2) 0 wit inspect .018 5.0
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect .17  11 1.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 14     260  
float-benchs/image_filter_true-unreach-call.c unknown 0 wit inspect .25  12 3.0  - 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/interpolation2_true-unreach-call_true-termination.c unknown 0 wit inspect .20  11 2.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .024 4.9
float-benchs/interpolation_true-unreach-call_true-termination.c unknown 0 wit inspect .17  11 1.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 4.8
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c unknown 0 wit inspect .18  11 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect .16  12 1.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 22     310  
float-benchs/inv_square_true-unreach-call_true-termination.c unknown 0 wit inspect .18  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .018 5.0
float-benchs/loop_true-unreach-call.c true 2 wit inspect 11     290 150    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 timeout 0 wit inspect 960     1200  
float-benchs/mea8000_true-unreach-call.c timeout (timeout) 0 wit inspect 900     67 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .020 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c unknown 0 wit inspect .18  11 2.0  - 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
float-benchs/nan_float_range_true-unreach-call_true-termination.c unknown 0 wit inspect .18  11 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900     61 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 44 error (2) 0 wit inspect .021 4.8
float-benchs/rlim_invariant_true-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900     61 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c unknown 0 wit inspect .19  11 2.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .022 4.9
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c unknown 0 wit inspect .17  11 2.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .020 4.9
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c unknown 0 wit inspect .17  11 2.1  - 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
float-benchs/sin_interpolated_negation_true-unreach-call.c unknown 0 wit inspect .20  11 2.2  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9
float-benchs/sin_interpolated_smallrange_true-unreach-call.c unknown 0 wit inspect .17  11 2.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 5.0
float-benchs/sqrt_Householder_constant_true-unreach-call.c true 2 wit inspect .14  11 2.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 error (7) 0 wit inspect 270     3000  
float-benchs/sqrt_Householder_interval_true-unreach-call.c unknown 0 wit inspect .19  11 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .021 4.9
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c unknown 0 wit inspect .17  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .018 4.8
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c unknown 0 wit inspect .18  11 2.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .020 4.9
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c unknown 0 wit inspect .18  11 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .021 4.9
float-benchs/sqrt_poly_true-unreach-call_true-termination.c unknown 0 wit inspect .17  11 1.9  - 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
float-benchs/water_pid_true-unreach-call_true-termination.c true 2 wit inspect .16  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 error (7) 0 wit inspect 190     2800  
float-benchs/zonotope_2_true-unreach-call_true-termination.c true 2 wit inspect 1.0   34 14    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    810 timeout 0 wit inspect 960     2500  
float-benchs/zonotope_3_true-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900     73 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.8
float-benchs/zonotope_loose_true-unreach-call_true-termination.c unknown 0 wit inspect .19  11 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .020 4.8
float-benchs/zonotope_tight_true-unreach-call_true-termination.c unknown 0 wit inspect .18  11 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 4.9
floats-esbmc-regression/Double_div_true-unreach-call.i true 2 wit inspect .17  11 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  320 true 2 wit inspect 250     2700  
floats-esbmc-regression/Float_div_true-unreach-call.i true 2 wit inspect .17  11 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.6  280 true 2 wit inspect 160     570  
floats-esbmc-regression/ceil_nondet_true-unreach-call.i unknown 0 wit inspect .095 11 .81 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/ceil_true-unreach-call.i error 0 wit inspect .13  11 1.6  - 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-esbmc-regression/copysign_true-unreach-call.i error 0 wit inspect .14  11 1.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .025 4.8
floats-esbmc-regression/digits_for_true-unreach-call.i true 2 wit inspect .17  11 1.6  - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 4.2  260 timeout 0 wit inspect 960     3100  
floats-esbmc-regression/digits_while_true-unreach-call.i true 2 wit inspect .17  11 1.4  - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 3.7  260 timeout 0 wit inspect 960     2900  
floats-esbmc-regression/fabs_true-unreach-call.i error 0 wit inspect .12  11 1.2  - 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
floats-esbmc-regression/fdim_true-unreach-call.i error 0 wit inspect .12  11 1.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .024 5.0
floats-esbmc-regression/floor_nondet_true-unreach-call.i unknown 0 wit inspect .096 11 .98 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .017 4.9
floats-esbmc-regression/floor_true-unreach-call.i error 0 wit inspect .12  11 1.2  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .022 4.8
floats-esbmc-regression/fmax_true-unreach-call.i error 0 wit inspect .14  11 1.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .022 5.0
floats-esbmc-regression/fmin_true-unreach-call.i error 0 wit inspect .14  11 1.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .023 5.0
floats-esbmc-regression/fmod2_true-unreach-call.i error 0 wit inspect .12  11 1.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .019 4.8
floats-esbmc-regression/fmod3_true-unreach-call.i error 0 wit inspect .13  11 1.2  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file)