BENCHMARK INFORMATION benchmark definition: run_definitions/yices2_model_QF_LinearRealArith.xml name: yices2_model_QF_LinearRealArith run sets: Yices2,5,ModelValidation.task date: Mon, 2025-06-23 18:05:44 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 1 with options 'unpack/9a71a8be5336a24d9219bd7598075f7ba06f85484bb819f3e8992e68a0a0d6cd/yices_smt2' and propertyfile 'benchmarks/properties/SMT.prp' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------------------------------------------------------- QF_LRA/QF_LRA_2019-ezsmt__travellingSalesperson_rand_70_300_1155482584_8.lp.yml true 0.13 0.13 ws04 QF_LRA/QF_LRA_DTP-Scheduling_constraints-temporal-machine-shop-2-3-A03.yml true 0.00 0.00 ws04 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_eric.t2.c_Iteration1_Lasso_4-pieceTemplate.yml TIMEOUT 61.00 61.01 ws15 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_eric2.t2.c_Iteration3_Loop_7-phaseTemplate.yml true 0.96 0.96 ws15 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_fir.t2.c_Iteration4_Loop_7-phaseTemplate.yml true 25.37 25.37 tc05 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_ludcmp.t2.c_Iteration9_Loop_7-phaseTemplate.yml TIMEOUT 61.00 61.01 ws04 QF_LRA/QF_LRA_LassoRanker__Ultimate_CooperatingT2_consts1.bpl_Iteration1_Lasso_7-phaseTemplate.yml true 4.36 4.36 tc04 QF_LRA/QF_LRA_LassoRanker__Ultimate_yPositive-SIscaled75.bpl_Iteration1_Loop_4-phaseTemplate.yml true 0.20 0.20 tc07 QF_LRA/QF_LRA_meti-tarski__Chua__1__IL__L_Chua-1-IL-L-chunk-0028.yml true 0.00 0.00 tc04 QF_LRA/QF_LRA_meti-tarski__Chua__1__IL__L_Chua-1-IL-L-chunk-0142.yml true 0.00 0.00 tc07 QF_LRA/QF_LRA_meti-tarski__Chua__1__VC1__U_Chua-1-VC1-U-chunk-0037.yml true 0.00 0.00 tc07 QF_LRA/QF_LRA_meti-tarski__bottom-plate-mixer_bottom-plate-mixer-chunk-0015.yml true 0.00 0.00 ws05 QF_LRA/QF_LRA_meti-tarski__bottom-plate-mixer_bottom-plate-mixer-chunk-0035.yml true 0.00 0.00 tc01 QF_LRA/QF_LRA_meti-tarski__cbrt__3_cbrt-problem-3-chunk-0035.yml true 0.00 0.00 tc07 QF_LRA/QF_LRA_meti-tarski__polypaver__bench-exp-3d_polypaver-bench-exp-3d-chunk-0050.yml true 0.00 0.00 ws18 QF_LRA/QF_LRA_meti-tarski__sin__problem__7__weak_sin-problem-7-weak-chunk-0070.yml true 0.00 0.00 tc04 QF_LRA/QF_LRA_meti-tarski__sqrt__1mcosq__7_sqrt-1mcosq-7-chunk-0103.yml true 0.00 0.01 tc07 QF_LRA/QF_LRA_sal__carpark_Carpark2-t1-4.yml true 0.01 0.01 tc02 QF_LRA/QF_LRA_sc_sc-27.induction.cvc.yml true 0.04 0.04 tc04 QF_LRA/QF_LRA_tta_startup_simple_startup_12nodes.bug.induct.yml true 1.06 1.06 tc01 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking06.yml true 0.01 0.01 ws05 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking17.yml true 0.03 0.03 tc02 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking19.yml true 0.03 0.03 tc02 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking22.yml true 0.04 0.05 ws15 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tempo-matrix2x2.pddl.yml true 0.76 0.76 ws05 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tempo-width-1.yml true 0.00 0.00 tc02 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tms-2-3-light-04.yml true 0.01 0.01 tc02 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tms-2-3-light-06.yml true 0.01 0.01 tc04 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tms-2-3-light-70.yml true 2.27 2.27 tc07 QF_RDL/QF_RDL_scheduling_abz6_943.yml true 0.30 0.30 ws16 QF_RDL/QF_RDL_scheduling_orb01_1059.yml true 12.47 12.47 ws16 QF_RDL/QF_RDL_scheduling_orb02_900.yml true 0.22 0.22 tc07 QF_RDL/QF_RDL_scheduling_orb03_1005.yml true 53.74 53.74 tc06 QF_RDL/QF_RDL_scheduling_orb03_1100.yml true 0.36 0.36 tc07 QF_RDL/QF_RDL_scheduling_orb06_1100.yml true 0.20 0.20 ws05 QF_RDL/QF_RDL_scheduling_orb07_550.yml true 0.02 0.02 ws04 QF_RDL/QF_RDL_scheduling_orb10_1100.yml true 0.03 0.03 ws18 QF_RDL/QF_RDL_scheduling_yn3_950.yml TIMEOUT 61.00 61.01 ws04 QF_RDL/QF_RDL_skdmxa2_skdmxa-3x3-14.induction.cvc.yml true 1.55 1.55 tc02 QF_RDL/QF_RDL_skdmxa2_skdmxa-3x3-5.induction.cvc.yml true 0.14 0.14 tc07 ------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 69.46 - Statistics: 40 Files correct: 36 correct true: 36 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 3