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: Thu, 2023-02-16 10:50:00 UTC tool: Goblint heads/yaml-witness-unassume-bench-0-g98c2a85b0 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-location/ourtool.2023-02-16_10-30-56.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-location/ourtool.2023-02-16_10-30-56.files/${rundefinition_name}/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------- as-hybrid.yml unknown 0.11 0.11 None bh-ex-add.yml unknown 0.18 0.19 None bh-ex1-poly.yml unknown 0.16 0.16 None bh-ex3.yml unknown 0.15 0.15 None hh-ex1b.yml true 0.12 0.13 None hh-ex2b.yml unknown 0.09 0.10 None hh-ex3.yml unknown 0.16 0.16 None mine-tutorial-ex4.10.yml true 0.09 0.10 None mine-tutorial-ex4.6.yml unknown 0.09 0.10 None mine-tutorial-ex4.7.yml unknown 0.12 0.13 None mine-tutorial-ex4.8.yml true 0.09 0.09 None ----------------------------------------------------------------------------------------- Run set 1 done 1.59 0.58 - 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-location/convert-tmp.2023-02-16_10-47-42.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-location/convert-tmp.2023-02-16_10-47-42.files/${rundefinition_name}/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------- as-hybrid.yml unknown 2.43 2.43 None bh-ex-add.yml EXCEPTION (Failure) 0.06 0.07 None bh-ex1-poly.yml unknown 11.32 11.32 None bh-ex3.yml EXCEPTION (Failure) 0.06 0.07 None hh-ex1b.yml EXCEPTION (Failure) 0.07 0.07 None hh-ex2b.yml unknown 16.37 16.39 None hh-ex3.yml TIMEOUT 61.00 61.02 None mine-tutorial-ex4.10.yml unknown 1.04 1.08 None mine-tutorial-ex4.6.yml unknown 0.26 0.26 None mine-tutorial-ex4.7.yml unknown 0.11 0.11 None mine-tutorial-ex4.8.yml true 0.09 0.09 None ----------------------------------------------------------------------------------------- Run set 2 done 93.03 61.34 - 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-location/convert-tmp.2023-02-16_10-47-42.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-location/convert-tmp.2023-02-16_10-47-42.files/${rundefinition_name}/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------- as-hybrid.yml true 0.12 0.12 None bh-ex-add.yml true 0.15 0.16 None bh-ex1-poly.yml unknown 0.30 0.31 None bh-ex3.yml true 0.16 0.17 None hh-ex1b.yml unknown 0.11 0.11 None hh-ex2b.yml true 0.09 0.09 None hh-ex3.yml unknown 0.17 0.18 None mine-tutorial-ex4.10.yml true 0.10 0.10 None mine-tutorial-ex4.6.yml true 0.09 0.09 None mine-tutorial-ex4.7.yml true 0.10 0.11 None mine-tutorial-ex4.8.yml true 0.09 0.09 None ----------------------------------------------------------------------------------------- Run set 3 done 1.72 0.54 - Statistics: 33 Files correct: 12 correct true: 12 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 21 Score: 24 (max: 66)