Task filter


ULTIMATE Automizer 2023-10-05 15:51:16 CEST uautomizer.uautomizer-default.bv64-unsafe

Add filter for:

btor2-val 2024-01-22 18:50:05 CET btor2-val.uautomizer-default.bv64-unsafe

Add filter for:

CPA-witness2test 2023-10-06 19:48:24 CEST cpa-w2t.uautomizer-default.bv64-unsafe

Add filter for:

CProver witness2test 2023-10-06 19:47:33 CEST fshell-w2t.uautomizer-default.bv64-unsafe

Add filter for:

Summary Table Quantile Plot Scatter Plot Info

Benchmark Setup

ToolULTIMATE Automizer 0.2.3-6fd36663btor2-val CPA-witness2test 2.2.1-svn-44619CProver witness2test 0.2
Limitstimelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
Hostapollon*
OSLinux 5.15.0
SystemCPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3800 MHz, Turbo Boost: disabled; RAM: 33467 MB
Date of execution2023-10-05 15:51:16 CEST2024-01-22 18:50:05 CET2023-10-06 19:48:24 CEST2023-10-06 19:47:33 CEST
Run setuautomizer.uautomizer-default.bv64-unsafebtor2-val.uautomizer-default.bv64-unsafecpa-w2t.uautomizer-default.bv64-unsafefshell-w2t.uautomizer-default.bv64-unsafe
Options
  • --full-output
  • --violation
  • --no-cache-update
  • --witness ../../exp-results/verification/violation/uautomizer.2023-10-05_15-51-16.files/${rundefinition_name}/${taskdef_name}/witness.graphml
  • -setprop witness.checkProgramHash=false
  • -heap 10000M
  • -benchmark
  • -setprop analysis.summaryEdges=true
  • -setprop cpa.callstack.skipVoidRecursion=true
  • -setprop cpa.callstack.skipFunctionPointerRecursion=true
  • -witness ../../exp-results/verification/violation/uautomizer.2023-10-05_15-51-16.files/${rundefinition_name}/${taskdef_name}/witness.graphml
  • --graphml-witness ../../exp-results/verification/violation/uautomizer.2023-10-05_15-51-16.files/${rundefinition_name}/${taskdef_name}/witness.graphml
Propertiesunreach-call

Statistics

ULTIMATE Automizer 2023-10-05 15:51:16 CEST uautomizer.uautomizer-default.bv64-unsafe
btor2-val 2024-01-22 18:50:05 CET btor2-val.uautomizer-default.bv64-unsafe
CPA-witness2test 2023-10-06 19:48:24 CEST cpa-w2t.uautomizer-default.bv64-unsafe
CProver witness2test 2023-10-06 19:47:33 CEST fshell-w2t.uautomizer-default.bv64-unsafe
Click here to select columns
 
status
cputime
(s)
walltime
(s)
memory
(MB)
 
status
cputime
(s)
walltime
(s)
memory
(MB)
 
status
cputime
(s)
walltime
(s)
memory
(MB)
 
status
cputime
(s)
walltime
(s)
memory
(MB)
all results
456
383000
315000
3610000
456
794  
796  
17700
456
790
468
27000
456
69.6
69.7
924
local summary
-
-
7340
-
-
-
192  
-
-
-
4140
-
-
-
3430  
-
    correct results
31
3790
2250
35500
27
54.5
55.8
1310
0
-
-
-
24
53.7
53.7
582
        correct true
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-
        correct false
31
3790
2250
35500
27
54.5
55.8
1310
0
-
-
-
24
53.7
53.7
582
    incorrect results
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-
        incorrect true
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-
        incorrect false
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-

Generated by BenchExec 3.18-dev