BENCHMARK INFORMATION benchmark definition: run_definitions/yices2_parallel_QF_NonLinearRealArith.xml name: yices2_parallel_QF_NonLinearRealArith run sets: Yices2,8,Parallel.task date: Fri, 2025-06-27 00:08:22 CEST tool: Yices2 tool executable: /usr/bin/./false 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 ------------------------------------------------------------ Yices2,8,Parallel.task Run set 1 of 1 with options 'unpack/9a71a8be5336a24d9219bd7598075f7ba06f85484bb819f3e8992e68a0a0d6cd/yices2_parallel.py --yices ./yices_smt2 -n 128' and propertyfile 'benchmarks/properties/SMT.prp' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- QF_NRA_20161105-Sturm-MBO_mbo_E8E10.yml TIMEOUT 487.96 61.05 tc01 QF_NRA_20170501-Heizmann-UltimateInvariantSynthesis_down.i_4_5_5.bpl_3.yml true 303.98 38.13 tc02 QF_NRA_20170501-Heizmann-UltimateInvariantSynthesis_gj2007.c.i_4_3_3.bpl_5.yml TIMEOUT 487.98 61.04 tc04 QF_NRA_20170501-Heizmann-UltimateInvariantSynthesis_nested9.i_5_6_6.bpl_3.yml TIMEOUT 488.51 61.04 tc08 QF_NRA_20170501-Heizmann-UltimateInvariantSynthesis_standard_allDiff2_ground.i_4_4_3.bpl_3.yml TIMEOUT 488.09 61.06 tc02 QF_NRA_20170501-Heizmann-UltimateInvariantSynthesis_standard_two_index_05.i_3_2_2.bpl_5.yml TIMEOUT 488.45 61.05 tc04 QF_NRA_20170501-Heizmann-UltimateInvariantSynthesis_standard_two_index_06.i_3_2_2.bpl_5.yml TIMEOUT 488.11 61.05 tc08 QF_NRA_LassoRanker__SV-COMP_BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.yml OUT OF MEMORY 64.47 8.03 tc06 QF_NRA_LassoRanker__SV-COMP_LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_4-pieceTemplate.yml OUT OF MEMORY 106.85 13.24 tc02 QF_NRA_LassoRanker__Ultimate_Braverman-2006CAV-Ex1-int.bpl_Iteration1_Lasso_6-phaseTemplate.yml TIMEOUT 488.14 61.04 tc05 QF_NRA_LassoRanker__Ultimate_yPositive-SIscaled75.bpl_Iteration1_Loop_4-pieceTemplate.yml OUT OF MEMORY 170.74 21.30 tc03 QF_NRA_hycomp_ball_count_2d_hill.02.redlog_global_8.yml TIMEOUT 488.34 61.04 tc05 QF_NRA_hycomp_ball_count_2d_hill.02.seq_lazy_lemmas_global_12.yml TIMEOUT 487.77 61.05 tc05 QF_NRA_hycomp_ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_10.yml TIMEOUT 488.31 61.04 tc06 QF_NRA_hycomp_ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_12.yml TIMEOUT 487.87 61.04 tc03 QF_NRA_hycomp_ball_count_2d_hill.03.seq_lazy_global_10.yml TIMEOUT 488.38 61.04 tc02 QF_NRA_hycomp_ball_count_2d_hill.03.seq_lazy_lemmas_global_10.yml TIMEOUT 488.03 61.04 tc02 QF_NRA_hycomp_ball_count_2d_hill.04.seq_lazy_global_14.yml TIMEOUT 488.05 61.05 tc01 QF_NRA_hycomp_ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_12.yml TIMEOUT 488.02 61.06 tc02 QF_NRA_hycomp_ball_count_2d_hill.05.redlog_global_12.yml TIMEOUT 487.81 61.05 tc03 QF_NRA_hycomp_ball_count_2d_hill.05.redlog_global_14.yml TIMEOUT 488.60 61.04 tc08 QF_NRA_hycomp_ball_count_2d_hill_simple.03.redlog_global_12.yml TIMEOUT 481.80 233.22 tc07 QF_NRA_hycomp_ball_count_2d_plain.03.redlog_global_14.yml TIMEOUT 488.10 61.05 tc04 QF_NRA_hycomp_ball_count_2d_slope.02.seq_lazy_global_12.yml TIMEOUT 488.68 61.05 tc01 QF_NRA_hycomp_ball_count_2d_slope.02.seq_lazy_linear_enc_global_14.yml TIMEOUT 488.14 61.06 tc04 QF_NRA_hycomp_ball_count_2d_slope.03.seq_lazy_global_10.yml TIMEOUT 487.80 61.05 tc02 QF_NRA_hycomp_ball_count_2d_slope.03.seq_lazy_lemmas_global_14.yml TIMEOUT 488.69 61.05 tc01 QF_NRA_hycomp_ball_count_2d_slope.03.seq_lazy_linear_enc_global_12.yml TIMEOUT 488.13 61.05 tc03 QF_NRA_hycomp_ball_count_2d_slope.03.seq_lazy_linear_enc_global_14.yml TIMEOUT 488.10 61.04 tc08 QF_NRA_hycomp_ball_count_2d_slope.04.seq_lazy_global_14.yml TIMEOUT 488.00 61.03 tc06 QF_NRA_hycomp_ball_count_2d_slope.05.seq_lazy_global_14.yml TIMEOUT 488.64 61.05 tc07 QF_NRA_hycomp_simple_ballistics_reach.01.seq_lazy_global_7.yml TIMEOUT 488.02 61.04 tc01 QF_NRA_hycomp_simple_ballistics_reach.01.seq_lazy_lemmas_global_15.yml TIMEOUT 488.64 61.05 tc07 QF_NRA_hycomp_simple_ballistics_reach.01.seq_lazy_lemmas_global_5.yml TIMEOUT 488.01 61.04 tc06 QF_NRA_hycomp_simple_ballistics_reach.01.seq_lazy_linear_enc_global_13.yml TIMEOUT 487.62 61.04 tc05 QF_NRA_hycomp_simple_ballistics_reach.01.seq_lazy_linear_enc_global_9.yml TIMEOUT 487.88 61.05 tc03 QF_NRA_hycomp_simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_15.yml TIMEOUT 488.53 61.04 tc07 QF_NRA_hycomp_simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_5.yml TIMEOUT 488.09 61.05 tc03 QF_NRA_kissing_kissing_3_11.yml TIMEOUT 488.31 61.06 tc02 QF_NRA_kissing_kissing_3_12.yml TIMEOUT 487.92 61.04 tc03 QF_NRA_kissing_kissing_4_15.yml TIMEOUT 488.37 61.04 tc08 QF_NRA_kissing_kissing_4_18.yml TIMEOUT 488.05 61.04 tc06 QF_NRA_kissing_kissing_4_24.yml TIMEOUT 488.92 61.04 tc08 QF_NRA_zankl_matrix-2-all-11.yml TIMEOUT 488.45 61.06 tc04 QF_NRA_zankl_matrix-2-all-13.yml TIMEOUT 488.33 61.05 tc05 QF_NRA_zankl_matrix-2-all-7.yml TIMEOUT 488.43 61.04 tc04 QF_NRA_zankl_matrix-4-all-10.yml TIMEOUT 488.24 61.04 tc06 QF_NRA_zankl_matrix-4-all-14.yml TIMEOUT 488.69 61.04 tc07 QF_NRA_zankl_matrix-4-all-18.yml OUT OF MEMORY 361.37 45.16 tc06 QF_NRA_zankl_matrix-4-all-6.yml TIMEOUT 488.40 61.08 tc01 QF_NRA_zankl_matrix-5-all-10.yml TIMEOUT 488.20 61.04 tc06 QF_NRA_zankl_matrix-5-all-8.yml TIMEOUT 489.22 61.05 tc05 ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None None - Statistics: 52 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 51