Task filter


CPAchecker 2023-10-04 13:45:46 CEST cpachecker.cpachecker-imc.bv64-safe

Add filter for:

btor2-val 2024-01-22 18:50:13 CET btor2-val-inductive.cpachecker-imc.bv64-safe

Add filter for:

btor2-val 2024-01-22 18:50:11 CET btor2-val-safe.cpachecker-imc.bv64-safe

Add filter for:

btor2-val 2024-01-22 18:50:09 CET btor2-val-valid.cpachecker-imc.bv64-safe

Add filter for:

liv 2023-10-06 22:30:55 CEST liv.cpachecker-imc.bv64-safe

Add filter for:

Summary Table Quantile Plot Scatter Plot Info

Benchmark Setup

ToolCPAchecker 2.2.1-svn-44619btor2-val liv 0.1-dev
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-04 13:45:46 CEST2024-01-22 18:50:13 CET2024-01-22 18:50:11 CET2024-01-22 18:50:09 CET2023-10-06 22:30:55 CEST
Run setcpachecker.cpachecker-imc.bv64-safebtor2-val-inductive.cpachecker-imc.bv64-safebtor2-val-safe.cpachecker-imc.bv64-safebtor2-val-valid.cpachecker-imc.bv64-safeliv.cpachecker-imc.bv64-safe
Options
  • -heap 13000M
  • -benchmark
  • -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true
  • -setprop cpa.arg.proofWitness=witness.graphml
  • -setprop cpa.arg.compressWitness=false
  • -setprop cpa.arg.witness.minimizeARG=false
  • -bmc-interpolation
  • --level inductive
  • --correctness
  • --no-cache-update
  • --hw-verifiers abc
  • --witness ../../exp-results/verification/correctness/cpachecker.2023-10-04_13-45-46.files/${rundefinition_name}/${taskdef_name}/witness.graphml
  • --level safe
  • --correctness
  • --no-cache-update
  • --hw-verifiers abc
  • --witness ../../exp-results/verification/correctness/cpachecker.2023-10-04_13-45-46.files/${rundefinition_name}/${taskdef_name}/witness.graphml
  • --level valid
  • --correctness
  • --no-cache-update
  • --hw-verifiers abc
  • --witness ../../exp-results/verification/correctness/cpachecker.2023-10-04_13-45-46.files/${rundefinition_name}/${taskdef_name}/witness.graphml
  • --stats
  • --no-cache-update
  • --cache-dir lib/cvt_cache/
  • --verifier actors/cbmc.yml
  • --verifierversion default
  • --allow-missing-invariant
  • --all-possible-invariant-locations
  • --fuzzy-invariant-locations 1
  • --witness ../../exp-results/verification/correctness/cpachecker.2023-10-04_13-45-46.files/${rundefinition_name}/${taskdef_name}/witness.graphml
Propertiesunreach-call

Statistics

CPAchecker 2023-10-04 13:45:46 CEST cpachecker.cpachecker-imc.bv64-safe
btor2-val 2024-01-22 18:50:13 CET btor2-val-inductive.cpachecker-imc.bv64-safe
btor2-val 2024-01-22 18:50:11 CET btor2-val-safe.cpachecker-imc.bv64-safe
btor2-val 2024-01-22 18:50:09 CET btor2-val-valid.cpachecker-imc.bv64-safe
liv 2023-10-06 22:30:55 CEST liv.cpachecker-imc.bv64-safe
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)
 
status
cputime
(s)
walltime
(s)
memory
(MB)
all results
758
556000
543000
2750000
758
4040
4080
43600
758
4840
4870
39600
758
8240
8260
42700
758
4940
4980
94400
local summary
-
-
37600
-
-
-
1090
-
-
-
1070
-
-
-
1060
-
-
-
1070
-
    correct results
119
14100
13100
116000
28
192
203
2500
27
193
199
2430
77
1430
1440
12500
15
235
242
12200
        correct true
119
14100
13100
116000
28
192
203
2500
27
193
199
2430
77
1430
1440
12500
15
235
242
12200
        correct false
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-
    incorrect results
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-
        incorrect true
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-
        incorrect false
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-
0
-
-
-

Generated by BenchExec 3.18-dev