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-04-11 07:13:10 UTC tool: Goblint heads/master-0-g317c88374 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: 4 resource limits: - memory: 6000.0 MB - time: 900 s - cpu cores: 1 hardware requirements: - cpu cores: 1 - memory: 6000.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-x/ourtool.2023-04-11_06-51-58.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-x/ourtool.2023-04-11_06-51-58.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.16 0.16 None bh-ex1-poly.yml unknown 0.15 0.15 None bh-ex3.yml unknown 0.15 0.15 None hh-ex1b.yml true 0.13 0.13 None hh-ex2b.yml unknown 0.11 0.11 None hh-ex3.yml unknown 0.15 0.15 None mine-tutorial-ex4.10.yml true 0.10 0.10 None mine-tutorial-ex4.6.yml unknown 0.09 0.09 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 1 done 1.53 0.99 - 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-x/convert-tmp.2023-04-11_07-08-46.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-x/convert-tmp.2023-04-11_07-08-46.files/${rundefinition_name}/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------- as-hybrid.yml unknown 2.36 2.36 None bh-ex-add.yml EXCEPTION (Failure) 0.07 0.07 None bh-ex1-poly.yml unknown 4.00 4.00 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 16.77 16.78 None hh-ex3.yml TIMEOUT 901.00 901.07 None mine-tutorial-ex4.10.yml unknown 1.09 1.09 None mine-tutorial-ex4.6.yml unknown 0.29 0.29 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 926.13 901.86 - 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-x/convert-tmp.2023-04-11_07-08-46.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-x/convert-tmp.2023-04-11_07-08-46.files/${rundefinition_name}/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------- as-hybrid.yml true 0.11 0.11 None bh-ex-add.yml true 0.15 0.15 None bh-ex1-poly.yml unknown 0.30 0.30 None bh-ex3.yml true 0.14 0.14 None hh-ex1b.yml unknown 0.12 0.16 None hh-ex2b.yml true 0.10 0.15 None hh-ex3.yml unknown 0.15 0.17 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.11 0.11 None mine-tutorial-ex4.8.yml true 0.09 0.09 None ----------------------------------------------------------------------------------------- Run set 3 done 1.70 1.10 - 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)