BENCHMARK INFORMATION benchmark definition: /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/ourtool-validate-tmp.xml name: ourtool-validate-tmp run sets: ourtool.Prec, cpachecker.Prec, uautomizer.Prec date: Tue, 2023-01-31 11:37:14 UTC tool: Goblint heads/yaml-witness-unassume-bench-0-g353653ad6-dirty tool executable: ./goblint options: --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra parallel runs: 14 resource limits: - memory: 1000.0 MB - time: 60 s - cpu cores: 1 hardware requirements: - cpu cores: 1 - memory: 1000.0 MB ------------------------------------------------------------ SYSTEM INFORMATION host: goblint-new os: Linux-5.15.0-52-generic-x86_64-with-glibc2.35 cpu: AMD EPYC Processor (with IBPB) - cores: 16 - max frequency: 2250.0 MHz ram: 33662.087168 MB ------------------------------------------------------------ ourtool.Prec Run set 1 of 3 with options '--conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set ana.activated[+] apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-guide/ourtool.2023-01-31_11-27-32.files/${rundefinition_name}/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------- as-hybrid.yml unknown 0.12 0.12 None bh-ex-add.yml unknown 0.17 0.17 None bh-ex1-poly.yml unknown 0.15 0.15 None bh-ex3.yml unknown 0.16 0.16 None hh-ex1b.yml true 0.15 0.15 None hh-ex2b.yml unknown 0.09 0.09 None hh-ex3.yml unknown 0.17 0.17 None mine-tutorial-ex4.10.yml true 0.10 0.10 None mine-tutorial-ex4.6.yml unknown 0.09 0.10 None mine-tutorial-ex4.7.yml unknown 0.12 0.12 None mine-tutorial-ex4.8.yml true 0.09 0.09 None ----------------------------------------------------------------------------------------- Run set 1 done 1.60 0.50 - cpachecker.Prec Run set 2 of 3 with options '--conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set ana.activated[+] apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-guide/convert-tmp.2023-01-31_11-34-58.files/${rundefinition_name}/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------- as-hybrid.yml true 0.66 0.66 None bh-ex-add.yml EXCEPTION (Failure) 0.07 0.08 None bh-ex1-poly.yml unknown 7.15 7.15 None bh-ex3.yml EXCEPTION (Failure) 0.07 0.07 None hh-ex1b.yml true 0.15 0.16 None hh-ex2b.yml true 6.71 6.72 None hh-ex3.yml TIMEOUT 61.04 61.05 None mine-tutorial-ex4.10.yml true 0.68 0.68 None mine-tutorial-ex4.6.yml true 0.14 0.14 None mine-tutorial-ex4.7.yml unknown 0.12 0.12 None mine-tutorial-ex4.8.yml true 0.10 0.10 None ----------------------------------------------------------------------------------------- Run set 2 done 77.09 61.33 - uautomizer.Prec Run set 3 of 3 with options '--conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set ana.activated[+] apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-guide/convert-tmp.2023-01-31_11-34-58.files/${rundefinition_name}/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------- as-hybrid.yml true 0.11 0.12 None bh-ex-add.yml true 0.18 0.19 None bh-ex1-poly.yml true 0.25 0.25 None bh-ex3.yml true 0.17 0.17 None hh-ex1b.yml true 0.13 0.14 None hh-ex2b.yml true 0.10 0.11 None hh-ex3.yml true 0.16 0.16 None mine-tutorial-ex4.10.yml true 0.11 0.12 None mine-tutorial-ex4.6.yml true 0.08 0.09 None mine-tutorial-ex4.7.yml true 0.11 0.11 None mine-tutorial-ex4.8.yml true 0.10 0.10 None ----------------------------------------------------------------------------------------- Run set 3 done 1.73 0.50 - Statistics: 33 Files correct: 20 correct true: 20 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 13 Score: 40 (max: 66)