BENCHMARK INFORMATION benchmark definition: run_definitions/smts_parallel_QF_LinearRealArith.xml name: smts_parallel_QF_LinearRealArith run sets: SMTS,0,Parallel.task date: Sun, 2025-06-29 13:54:48 CEST tool: SMTS tool executable: ./unpack/1e2d91adb57ec6ad11e88969089e1cec9341b824f2bce2f3826a08d0d6aa2783/SMTS/server/smts.py options: property file: benchmarks/properties/SMT.prp resource limits: - memory: 8192.0 MB - time: 480 s - cpu cores: 8 hardware requirements: - cpu model: Intel Core i7 - cpu cores: 8 - memory: 8192.0 MB ------------------------------------------------------------ SMTS,0,Parallel.task Run set 1 of 1 with options 'unpack/1e2d91adb57ec6ad11e88969089e1cec9341b824f2bce2f3826a08d0d6aa2783/SMTS/server/smts.py -l -p -pt 2 -o 64 -fp' and propertyfile 'benchmarks/properties/SMT.prp' inputfile status cpu time wall time host --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- QF_LRA/QF_LRA_2017-Heizmann-UltimateInvariantSynthesis__array_ptr_single_elem_init.i_4_2_2.bpl_7.yml false 53.18 6.73 tc01 QF_LRA/QF_LRA_2017-Heizmann-UltimateInvariantSynthesis__gj2007.c.i_4_3_3.bpl_11.yml TIMEOUT 488.02 61.05 tc08 QF_LRA/QF_LRA_2017-Heizmann-UltimateInvariantSynthesis__overflow1.i_3_8_2.bpl_11.yml TIMEOUT 487.87 61.04 tc02 QF_LRA/QF_LRA_2017-Heizmann-UltimateInvariantSynthesis__sanfoundry_10_ground.i_6_3_3.bpl_13.yml OUT OF MEMORY 41.58 5.24 ws02 QF_LRA/QF_LRA_2019-ezsmt__Labyrinth__SCC_Strong_0198-labyrinth-19-0.yml OUT OF MEMORY 22.89 7.92 tc08 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_brp_withassume.t2.c_Iteration8_Loop_4-pieceTemplate.yml OUT OF MEMORY 36.99 6.05 ws02 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_brp_withassume.t2.c_Iteration8_Loop_6-phaseTemplate.yml OUT OF MEMORY 36.92 4.93 tc06 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_brp_withassume.t2.c_Iteration8_Loop_7-phaseTemplate.yml OUT OF MEMORY 33.87 4.84 tc06 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_eric.t2.c_Iteration1_Lasso_4-pieceTemplate.yml TIMEOUT 488.48 61.03 tc02 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_ex11.t2.c_Iteration1_Lasso_3-pieceTemplate.yml TIMEOUT 488.55 61.05 tc05 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_ex11.t2.c_Iteration1_Lasso_4-pieceTemplate.yml OUT OF MEMORY 178.71 22.34 tc02 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_firewire.t2.c_Iteration1_Lasso_4-pieceTemplate.yml OUT OF MEMORY 40.23 5.62 tc02 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_firewire.t2.c_Iteration1_Lasso_6-phaseTemplate.yml OUT OF MEMORY 51.73 6.49 tc02 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_firewire.t2.c_Iteration1_Lasso_7-phaseTemplate.yml OUT OF MEMORY 36.90 4.77 ws02 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_hongyi1.t2.c_Iteration1_Loop_4-pieceTemplate.yml OUT OF MEMORY 37.63 5.63 tc06 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_hongyi1.t2.c_Iteration9_Loop_4-pieceTemplate.yml OUT OF MEMORY 37.46 5.72 tc06 QF_LRA/QF_LRA_LassoRanker__CooperatingT2_hongyi1.t2.c_Iteration9_Loop_7-phaseTemplate.yml OUT OF MEMORY 36.14 5.64 tc01 QF_LRA/QF_LRA_LassoRanker__SV-COMP_GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.yml OUT OF MEMORY 38.17 5.77 tc02 QF_LRA/QF_LRA_LassoRanker__SV-COMP_LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_4-pieceTemplate.yml TIMEOUT 488.89 61.05 tc06 QF_LRA/QF_LRA_LassoRanker__SV-COMP_LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_7-phaseTemplate.yml TIMEOUT 488.74 61.07 tc06 QF_LRA/QF_LRA_LassoRanker__SV-COMP_TelAviv-Amir-Minimum_true-termination.c_Iteration1_Lasso_4-pieceTemplate.yml OUT OF MEMORY 36.46 5.96 tc04 QF_LRA/QF_LRA_LassoRanker__SV-COMP_TelAviv-Amir-Minimum_true-termination.c_Iteration1_Loop_4-pieceTemplate.yml OUT OF MEMORY 36.70 5.93 tc02 QF_LRA/QF_LRA_LassoRanker__Ultimate_Braverman-2006CAV-Ex1-int.bpl_Iteration1_Lasso_7-phaseTemplate.yml TIMEOUT 487.75 61.02 tc08 QF_LRA/QF_LRA_LassoRanker__Ultimate_Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_7-phaseTemplate.yml TIMEOUT 487.81 61.03 tc05 QF_LRA/QF_LRA_LassoRanker__Ultimate_MenloPark.bpl_Iteration1_Lasso_4-pieceTemplate.yml TIMEOUT 487.87 61.04 tc04 QF_LRA/QF_LRA_LassoRanker__Ultimate_OpposedDisjuncts.bpl_Iteration1_Lasso_4-pieceTemplate.yml TIMEOUT 488.92 61.04 tc02 QF_LRA/QF_LRA_miplib_danoint-65.yml TIMEOUT 487.94 61.04 tc04 QF_LRA/QF_LRA_miplib_danoint-66.yml TIMEOUT 487.81 61.02 tc02 QF_LRA/QF_LRA_miplib_fixnet-3000.yml TIMEOUT 487.98 61.04 tc01 QF_LRA/QF_LRA_miplib_fixnet-3983.yml TIMEOUT 487.87 61.04 tc01 QF_LRA/QF_LRA_miplib_opt1217--17.yml false 38.66 4.91 tc08 QF_LRA/QF_LRA_miplib_pk1-0.yml false 55.47 7.01 tc02 QF_LRA/QF_LRA_miplib_pk1-11.yml false 75.05 9.47 tc06 QF_LRA/QF_LRA_miplib_pp08a-5000.yml TIMEOUT 488.01 61.06 tc01 QF_LRA/QF_LRA_miplib_pp08a-7349.yml false 38.81 4.93 tc01 QF_LRA/QF_LRA_tropical-matrix_constraint-1007893.yml false 113.14 14.25 ws02 QF_LRA/QF_LRA_tropical-matrix_constraint-556101.yml TIMEOUT 488.49 61.03 tc08 QF_LRA/QF_LRA_tta_startup_simple_startup_15nodes.abstract.induct.yml TIMEOUT 486.79 61.03 ws02 QF_RDL/QF_RDL_scheduling_swv12_3004.yml OUT OF MEMORY 109.44 13.60 ws02 QF_RDL/QF_RDL_scheduling_swv12_3050.yml OUT OF MEMORY 114.61 14.38 tc08 QF_RDL/QF_RDL_scheduling_swv13_3000.yml OUT OF MEMORY 109.38 13.56 tc06 QF_RDL/QF_RDL_scheduling_swv13_3104.yml OUT OF MEMORY 107.34 13.35 tc05 QF_RDL/QF_RDL_scheduling_swv13_3150.yml OUT OF MEMORY 105.29 13.12 tc08 QF_RDL/QF_RDL_scheduling_swv13_3200.yml OUT OF MEMORY 111.18 13.79 tc04 QF_RDL/QF_RDL_scheduling_swv14_2800.yml OUT OF MEMORY 113.40 14.09 tc04 QF_RDL/QF_RDL_scheduling_swv14_2885.yml OUT OF MEMORY 107.92 13.37 tc05 QF_RDL/QF_RDL_scheduling_swv14_2895.yml OUT OF MEMORY 103.03 12.76 tc08 QF_RDL/QF_RDL_scheduling_swv14_2905.yml OUT OF MEMORY 98.14 12.25 ws02 QF_RDL/QF_RDL_scheduling_swv14_3000.yml OUT OF MEMORY 103.83 12.88 tc08 QF_RDL/QF_RDL_scheduling_yn1_827.yml TIMEOUT 488.01 61.03 tc06 QF_RDL/QF_RDL_scheduling_yn1_850.yml TIMEOUT 488.19 61.08 tc05 QF_RDL/QF_RDL_scheduling_yn1_887.yml false 265.94 33.39 ws02 QF_RDL/QF_RDL_scheduling_yn2_862.yml TIMEOUT 487.98 61.04 tc04 QF_RDL/QF_RDL_scheduling_yn2_890.yml false 323.17 40.55 ws02 QF_RDL/QF_RDL_scheduling_yn2_910.yml TIMEOUT 487.98 61.06 tc04 QF_RDL/QF_RDL_scheduling_yn3_828.yml TIMEOUT 487.84 61.02 tc06 QF_RDL/QF_RDL_scheduling_yn3_860.yml false 202.31 25.43 ws02 QF_RDL/QF_RDL_scheduling_yn3_894.yml TIMEOUT 488.01 61.04 tc04 QF_RDL/QF_RDL_scheduling_yn4_1000.yml TIMEOUT 487.97 61.04 tc02 QF_RDL/QF_RDL_scheduling_yn4_919.yml TIMEOUT 487.95 61.03 tc08 QF_RDL/QF_RDL_scheduling_yn4_950.yml false 155.48 19.51 tc01 QF_RDL/QF_RDL_scheduling_yn4_969.yml false 331.04 41.46 tc01 --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None None - Statistics: 62 Files correct: 3 correct true: 0 correct false: 3 incorrect: 1 incorrect true: 0 incorrect false: 1 unknown: 51