BENCHMARK INFORMATION benchmark definition: run_definitions/yices2_model_QF_NonLinearRealArith.xml name: yices2_model_QF_NonLinearRealArith run sets: Yices2,5,ModelValidation.task date: Mon, 2025-06-23 18:08:43 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_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_hints_escape25_POMC_hints.yml true 0.51 0.51 tc07 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_hints_mod5_POMC_hints.yml true 0.29 0.29 ws08 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_hints_mod7_POMC_hints.yml true 0.76 0.76 tc01 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_no_hints_escape25_POMC_no_hints.yml TIMEOUT 61.01 61.01 ws07 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_no_hints_mod5_POMC_no_hints.yml TIMEOUT 61.00 61.00 tc05 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_no_hints_mod7_POMC_no_hints.yml TIMEOUT 61.01 61.02 tc04 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__past_geom_offspring_0.499_PRAY.yml true 0.04 0.04 ws19 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__past_huge_runtime_PRAY.yml true 0.02 0.02 ws07 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__past_huge_runtime_tiny_probs_PRAY.yml true 0.01 0.01 tc07 QF_NRA_LassoRanker__CooperatingT2_polyrank5.t2.c_Iteration1_Loop_6-phaseTemplate.yml true 2.38 2.39 tc04 QF_NRA_hycomp_ball_count_2d_plain.02.seq_lazy_lemmas_global_6.yml true 0.03 0.03 ws07 QF_NRA_meti-tarski__Lyapunov_Lyapunov1a-chunk-0034.yml true 0.01 0.01 tc01 QF_NRA_meti-tarski__atan__problem__2__weak_atan-problem-2-weak-chunk-0177.yml true 0.01 0.01 ws19 QF_NRA_meti-tarski__atan__vega__3_atan-vega-3-chunk-0368.yml true 0.01 0.01 ws14 QF_NRA_meti-tarski__atan__vega__3_atan-vega-3-chunk-0547.yml true 0.01 0.01 tc04 QF_NRA_meti-tarski__cbrt__3__weak_cbrt-problem-3-weak-chunk-0062.yml true 0.01 0.01 tc05 QF_NRA_meti-tarski__cbrt__3__weak_cbrt-problem-3-weak-chunk-0090.yml true 0.01 0.01 ws19 QF_NRA_meti-tarski__polypaver__bench-sqrt-3d_polypaver-bench-sqrt-3d-chunk-0442.yml true 0.01 0.01 tc01 QF_NRA_meti-tarski__sqrt__1mcosq__7_sqrt-1mcosq-7-chunk-0178.yml true 0.01 0.01 tc01 QF_NRA_meti-tarski__sqrt__1mcosq__8_sqrt-1mcosq-8-chunk-0699.yml true 0.01 0.01 tc04 --------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 67.45 - Statistics: 20 Files correct: 17 correct true: 17 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 3