BENCHMARK INFORMATION benchmark definition: run_definitions/opensmt_model_QF_LinearRealArith.xml name: opensmt_model_QF_LinearRealArith run sets: OpenSMT,1,ModelValidation.task date: Mon, 2025-06-23 17:42:16 CEST tool: OpenSMT tool executable: ./unpack/ef2e8e3315254aac78ddc31cdf6813a5640ea2cb5bc2c7901a270d8285b95c79/opensmt 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 ------------------------------------------------------------ OpenSMT,1,ModelValidation.task Run set 1 of 1 with options 'unpack/ef2e8e3315254aac78ddc31cdf6813a5640ea2cb5bc2c7901a270d8285b95c79/opensmt' 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 22.27 22.28 ws04 QF_LRA/QF_LRA_DTP-Scheduling_constraints-temporal-machine-shop-2-3-A03.yml true 0.00 0.00 ws06 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_eric.t2.c_Iteration1_Lasso_4-pieceTemplate.yml TIMEOUT 61.00 61.01 ws10 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_eric2.t2.c_Iteration3_Loop_7-phaseTemplate.yml true 0.73 0.73 ws09 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_fir.t2.c_Iteration4_Loop_7-phaseTemplate.yml true 11.42 11.42 ws06 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_ludcmp.t2.c_Iteration9_Loop_7-phaseTemplate.yml TIMEOUT 61.01 61.01 ws02 QF_LRA/QF_LRA_LassoRanker__Ultimate_CooperatingT2_consts1.bpl_Iteration1_Lasso_7-phaseTemplate.yml true 1.14 1.14 tc04 QF_LRA/QF_LRA_LassoRanker__Ultimate_yPositive-SIscaled75.bpl_Iteration1_Loop_4-phaseTemplate.yml true 1.10 1.10 ws10 QF_LRA/QF_LRA_meti-tarski__Chua__1__IL__L_Chua-1-IL-L-chunk-0028.yml true 0.00 0.00 ws19 QF_LRA/QF_LRA_meti-tarski__Chua__1__IL__L_Chua-1-IL-L-chunk-0142.yml true 0.00 0.00 ws13 QF_LRA/QF_LRA_meti-tarski__Chua__1__VC1__U_Chua-1-VC1-U-chunk-0037.yml true 0.00 0.00 ws02 QF_LRA/QF_LRA_meti-tarski__bottom-plate-mixer_bottom-plate-mixer-chunk-0015.yml true 0.00 0.00 ws09 QF_LRA/QF_LRA_meti-tarski__bottom-plate-mixer_bottom-plate-mixer-chunk-0035.yml true 0.00 0.00 ws04 QF_LRA/QF_LRA_meti-tarski__cbrt__3_cbrt-problem-3-chunk-0035.yml true 0.00 0.00 tc04 QF_LRA/QF_LRA_meti-tarski__polypaver__bench-exp-3d_polypaver-bench-exp-3d-chunk-0050.yml true 0.00 0.00 ws06 QF_LRA/QF_LRA_meti-tarski__sin__problem__7__weak_sin-problem-7-weak-chunk-0070.yml true 0.00 0.00 ws05 QF_LRA/QF_LRA_meti-tarski__sqrt__1mcosq__7_sqrt-1mcosq-7-chunk-0103.yml true 0.00 0.00 ws04 QF_LRA/QF_LRA_sal__carpark_Carpark2-t1-4.yml true 0.02 0.02 ws09 QF_LRA/QF_LRA_sc_sc-27.induction.cvc.yml true 0.23 0.23 ws10 QF_LRA/QF_LRA_tta_startup_simple_startup_12nodes.bug.induct.yml true 1.04 1.04 ws05 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking06.yml true 0.02 0.02 ws09 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking17.yml true 0.06 0.06 ws06 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking19.yml true 0.07 0.07 ws13 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_cooking22.yml true 0.08 0.08 ws13 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tempo-matrix2x2.pddl.yml true 1.83 1.83 ws10 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tempo-width-1.yml true 0.00 0.01 ws04 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tms-2-3-light-04.yml true 0.02 0.02 ws05 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tms-2-3-light-06.yml true 0.03 0.03 ws13 QF_RDL/QF_RDL_SMT-Temporal-Planning-Benchmarks_tms-2-3-light-70.yml true 6.49 6.49 tc04 QF_RDL/QF_RDL_scheduling_abz6_943.yml true 4.55 4.55 ws19 QF_RDL/QF_RDL_scheduling_orb01_1059.yml TIMEOUT 61.00 61.00 ws17 QF_RDL/QF_RDL_scheduling_orb02_900.yml true 0.86 0.86 ws05 QF_RDL/QF_RDL_scheduling_orb03_1005.yml true 47.09 47.09 ws05 QF_RDL/QF_RDL_scheduling_orb03_1100.yml true 4.07 4.07 ws09 QF_RDL/QF_RDL_scheduling_orb06_1100.yml true 1.06 1.06 ws13 QF_RDL/QF_RDL_scheduling_orb07_550.yml true 0.09 0.09 ws06 QF_RDL/QF_RDL_scheduling_orb10_1100.yml true 0.22 0.22 ws06 QF_RDL/QF_RDL_scheduling_yn3_950.yml TIMEOUT 61.00 61.00 ws09 QF_RDL/QF_RDL_skdmxa2_skdmxa-3x3-14.induction.cvc.yml TIMEOUT 61.01 61.02 ws06 QF_RDL/QF_RDL_skdmxa2_skdmxa-3x3-5.induction.cvc.yml true 24.39 24.39 ws13 ------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 70.20 - Statistics: 40 Files correct: 34 correct true: 34 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5