BENCHMARK INFORMATION benchmark definition: run_definitions/yices2_model_QF_NonLinearIntArith.xml name: yices2_model_QF_NonLinearIntArith run sets: Yices2,5,ModelValidation.task, Yices2,6,ModelValidation.task date: Mon, 2025-06-23 18:07:31 CEST tool: Yices2 tool executable: /usr/bin/./false options: property file: benchmarks/properties/SMT.prp resource limits: - memory: 8192.0 MB - time: 240 s - cpu cores: 2 hardware requirements: - cpu model: Intel Core i7 - cpu cores: 2 - memory: 8192.0 MB ------------------------------------------------------------ Yices2,5,ModelValidation.task Run set 1 of 2 with options 'unpack/9a71a8be5336a24d9219bd7598075f7ba06f85484bb819f3e8992e68a0a0d6cd/yices_smt2' and propertyfile 'benchmarks/properties/SMT.prp' inputfile status cpu time wall time host ------------------------------------------------------------------------------------- ------------------------------------------------------------------------------------- Run set 1 done None 67.66 - Yices2,6,ModelValidation.task Run set 2 of 2 with options 'unpack/9a71a8be5336a24d9219bd7598075f7ba06f85484bb819f3e8992e68a0a0d6cd/yices_smt2 --mcsat-l2o' and propertyfile 'benchmarks/properties/SMT.prp' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ QF_NIA_20170427-VeryMax__CInteger_Stroeder_15__NonTermination1_false-termination.c__p24848_edge_closing_0.yml true 0.01 0.01 ws09 QF_NIA_20170427-VeryMax__ITS_From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31463_safety_0.yml true 3.90 3.90 tc07 QF_NIA_20170427-VeryMax__ITS_From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31642_safety_0.yml true 1.19 1.19 ws19 QF_NIA_20170427-VeryMax__ITS_From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31700_safety_0.yml true 0.54 0.54 ws09 QF_NIA_20170427-VeryMax__ITS_From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p2743_safety_0.yml true 3.10 3.10 tc06 QF_NIA_20170427-VeryMax__ITS_From_AProVE_2014__juLinkedListCreateAddAll.jar-obl-11__p9372_terminationG_0.yml true 2.34 2.34 ws19 QF_NIA_20170427-VeryMax__ITS_From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8542_safety_0.yml true 2.88 2.88 ws07 QF_NIA_20170427-VeryMax__ITS_From_T2__brp_withassume.t2__p17432_edge_closing_0.yml true 11.20 11.20 ws09 QF_NIA_20170427-VeryMax__ITS_From_T2__ex36.t2_fixed__p23163_safety_0.yml true 0.65 0.65 tc04 QF_NIA_20170427-VeryMax__ITS_From_T2__ex36.t2_fixed__p23397_safety_0.yml true 0.06 0.06 ws19 QF_NIA_20170427-VeryMax__ITS_From_T2__fun1.t2_fixed__p785_terminationG_0.yml TIMEOUT 61.01 61.01 tc04 QF_NIA_20170427-VeryMax__ITS_From_T2__s1-striped.t2__p13462_safety_0.yml true 0.90 0.91 ws07 QF_NIA_20170427-VeryMax__ITS_From_T2__s1-striped.t2__p13641_safety_0.yml true 1.57 1.57 ws04 QF_NIA_20170427-VeryMax__ITS_From_T2__s1.t2__p21154_safety_0.yml true 1.75 1.75 ws09 QF_NIA_20170427-VeryMax__SAT14_1298.yml true 0.62 0.62 ws07 QF_NIA_20170427-VeryMax__SAT14_1317.yml true 1.43 1.43 ws12 QF_NIA_20170427-VeryMax__SAT14_516.yml true 0.75 0.75 ws11 QF_NIA_20220315-MathProblems_MS_09.yml TIMEOUT 61.01 61.01 ws06 QF_NIA_AProVE_aproveSMT1834216988929529060.yml true 0.01 0.01 ws07 QF_NIA_AProVE_aproveSMT7293342508155251815.yml true 0.01 0.02 ws03 ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ Run set 2 done None 67.66 - Statistics: 20 Files correct: 18 correct true: 18 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 2