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 08:41:32 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/ourtool.2023-01-31_08-22-23.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit/ourtool.2023-01-31_08-22-23.files/${rundefinition_name}/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------- as-hybrid.yml unknown 0.11 0.13 None bh-ex-add.yml unknown 0.18 0.18 None bh-ex1-poly.yml unknown 0.16 0.16 None bh-ex3.yml unknown 0.16 0.16 None hh-ex1b.yml true 0.14 0.15 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.10 0.11 None mine-tutorial-ex4.6.yml unknown 0.11 0.11 None mine-tutorial-ex4.7.yml unknown 0.11 0.12 None mine-tutorial-ex4.8.yml true 0.10 0.10 None ----------------------------------------------------------------------------------------- Run set 1 done 1.64 0.49 - 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/convert-tmp.2023-01-31_08-39-19.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit/convert-tmp.2023-01-31_08-39-19.files/${rundefinition_name}/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------- as-hybrid.yml unknown 2.41 2.42 None bh-ex-add.yml EXCEPTION (Failure) 0.07 0.08 None bh-ex1-poly.yml unknown 11.60 11.60 None bh-ex3.yml EXCEPTION (Failure) 0.07 0.07 None hh-ex1b.yml EXCEPTION (Failure) 0.07 0.07 None hh-ex2b.yml unknown 17.05 17.05 None hh-ex3.yml TIMEOUT 61.01 61.02 None mine-tutorial-ex4.10.yml unknown 1.09 1.09 None mine-tutorial-ex4.6.yml unknown 0.27 0.27 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 2 done 94.06 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/convert-tmp.2023-01-31_08-39-19.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit/convert-tmp.2023-01-31_08-39-19.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.30 None bh-ex3.yml true 0.17 0.17 None hh-ex1b.yml unknown 0.12 0.12 None hh-ex2b.yml true 0.10 0.10 None hh-ex3.yml unknown 0.16 0.16 None mine-tutorial-ex4.10.yml true 0.10 0.11 None mine-tutorial-ex4.6.yml true 0.09 0.12 None mine-tutorial-ex4.7.yml true 0.12 0.13 None mine-tutorial-ex4.8.yml true 0.10 0.10 None ----------------------------------------------------------------------------------------- Run set 3 done 1.74 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)