BENCHMARK INFORMATION benchmark definition: run_definitions/cvc5_model_QF_LinearRealArith.xml name: cvc5_model_QF_LinearRealArith run sets: cvc5,2,ModelValidation.task date: Tue, 2025-06-24 13:32:47 CEST tool: cvc5 tool executable: ./unpack/1647fe1d9c9285ea0d2f2566270b82d066e64b381a008d32982da1d679391a6c/bin/starexec_run_sq 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 ------------------------------------------------------------ cvc5,2,ModelValidation.task Run set 1 of 1 with options 'unpack/1647fe1d9c9285ea0d2f2566270b82d066e64b381a008d32982da1d679391a6c/bin/starexec_run_mv' 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 TIMEOUT 61.02 61.00 ws07 QF_LRA/QF_LRA_DTP-Scheduling_constraints-temporal-machine-shop-2-3-A03.yml true 0.08 0.08 ws07 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_eric.t2.c_Iteration1_Lasso_4-pieceTemplate.yml TIMEOUT 61.02 61.00 tc05 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_eric2.t2.c_Iteration3_Loop_7-phaseTemplate.yml true 4.37 4.37 tc07 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_fir.t2.c_Iteration4_Loop_7-phaseTemplate.yml TIMEOUT 61.03 61.00 tc07 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_ludcmp.t2.c_Iteration9_Loop_7-phaseTemplate.yml TIMEOUT 61.03 61.00 ws07 QF_LRA/QF_LRA_LassoRanker__Ultimate_CooperatingT2_consts1.bpl_Iteration1_Lasso_7-phaseTemplate.yml true 9.41 9.41 ws07 QF_LRA/QF_LRA_LassoRanker__Ultimate_yPositive-SIscaled75.bpl_Iteration1_Loop_4-phaseTemplate.yml true 7.81 7.81 tc02 QF_LRA/QF_LRA_meti-tarski__Chua__1__IL__L_Chua-1-IL-L-chunk-0028.yml true 0.05 0.05 ws07 QF_LRA/QF_LRA_meti-tarski__Chua__1__IL__L_Chua-1-IL-L-chunk-0142.yml true 0.05 0.05 tc02 QF_LRA/QF_LRA_meti-tarski__Chua__1__VC1__U_Chua-1-VC1-U-chunk-0037.yml true 0.05 0.05 ws07 QF_LRA/QF_LRA_meti-tarski__bottom-plate-mixer_bottom-plate-mixer-chunk-0015.yml true 0.05 0.05 tc02 QF_LRA/QF_LRA_meti-tarski__bottom-plate-mixer_bottom-plate-mixer-chunk-0035.yml true 0.06 0.06 tc07 QF_LRA/QF_LRA_meti-tarski__cbrt__3_cbrt-problem-3-chunk-0035.yml true 0.05 0.05 tc05 QF_LRA/QF_LRA_meti-tarski__polypaver__bench-exp-3d_polypaver-bench-exp-3d-chunk-0050.yml true 0.07 0.07 ws07 QF_LRA/QF_LRA_meti-tarski__sin__problem__7__weak_sin-problem-7-weak-chunk-0070.yml true 0.06 0.06 tc07 QF_LRA/QF_LRA_meti-tarski__sqrt__1mcosq__7_sqrt-1mcosq-7-chunk-0103.yml true 0.06 0.06 tc07 QF_LRA/QF_LRA_sal__carpark_Carpark2-t1-4.yml true 0.10 0.10 tc07 QF_LRA/QF_LRA_sc_sc-27.induction.cvc.yml true 0.53 0.53 tc02 QF_LRA/QF_LRA_tta_startup_simple_startup_12nodes.bug.induct.yml true 2.34 2.34 tc08 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking06.yml true 0.09 0.09 tc02 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking17.yml true 0.28 0.28 ws07 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking19.yml true 0.36 0.36 ws07 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking22.yml true 0.43 0.42 ws07 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tempo-matrix2x2.pddl.yml TIMEOUT 60.92 61.00 tc01 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tempo-width-1.yml true 0.02 0.02 tc08 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tms-2-3-light-04.yml true 0.07 0.07 tc07 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tms-2-3-light-06.yml true 0.11 0.12 tc07 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tms-2-3-light-70.yml true 4.16 4.16 tc07 QF_RDL/QF_RDL_scheduling_abz6_943.yml true 1.28 1.28 ws07 QF_RDL/QF_RDL_scheduling_orb01_1059.yml TIMEOUT 61.01 61.00 tc07 QF_RDL/QF_RDL_scheduling_orb02_900.yml true 2.75 2.75 tc08 QF_RDL/QF_RDL_scheduling_orb03_1005.yml TIMEOUT 61.01 61.00 tc08 QF_RDL/QF_RDL_scheduling_orb03_1100.yml true 2.99 2.99 tc07 QF_RDL/QF_RDL_scheduling_orb06_1100.yml true 8.41 8.44 tc07 QF_RDL/QF_RDL_scheduling_orb07_550.yml true 0.30 0.30 tc07 QF_RDL/QF_RDL_scheduling_orb10_1100.yml true 0.68 0.68 ws07 QF_RDL/QF_RDL_scheduling_yn3_950.yml TIMEOUT 61.01 61.00 tc05 QF_RDL/QF_RDL_skdmxa2_skdmxa-3x3-14.induction.cvc.yml true 21.80 21.80 tc08 QF_RDL/QF_RDL_skdmxa2_skdmxa-3x3-5.induction.cvc.yml true 3.13 3.13 ws07 ------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 131.17 - Statistics: 40 Files correct: 32 correct true: 32 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 8