BENCHMARK INFORMATION benchmark definition: run_definitions/cvc5_model_QF_NonLinearRealArith.xml name: cvc5_model_QF_NonLinearRealArith run sets: cvc5,2,ModelValidation.task date: Tue, 2025-06-24 13:39:49 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_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_hints_escape25_POMC_hints.yml TIMEOUT 61.00 61.00 tc07 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_hints_mod5_POMC_hints.yml TIMEOUT 61.00 61.00 tc04 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_hints_mod7_POMC_hints.yml TIMEOUT 61.00 61.00 ws10 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_no_hints_escape25_POMC_no_hints.yml true 1.08 1.08 ws11 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_no_hints_mod5_POMC_no_hints.yml true 0.43 0.43 ws11 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__certificate_no_hints_mod7_POMC_no_hints.yml TIMEOUT 61.00 61.00 tc01 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__past_geom_offspring_0.499_PRAY.yml true 0.06 0.06 ws10 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__past_huge_runtime_PRAY.yml true 33.54 33.54 ws10 QF_NRA_20240407-pPDA-Chiari-Pontiggia-Winkler__past_huge_runtime_tiny_probs_PRAY.yml true 0.02 0.02 ws10 QF_NRA_LassoRanker__CooperatingT2_polyrank5.t2.c_Iteration1_Loop_6-phaseTemplate.yml true 0.16 0.16 ws10 QF_NRA_hycomp_ball_count_2d_plain.02.seq_lazy_lemmas_global_6.yml true 1.12 1.12 tc01 QF_NRA_meti-tarski__Lyapunov_Lyapunov1a-chunk-0034.yml true 0.01 0.01 ws10 QF_NRA_meti-tarski__atan__problem__2__weak_atan-problem-2-weak-chunk-0177.yml true 0.02 0.02 tc07 QF_NRA_meti-tarski__atan__vega__3_atan-vega-3-chunk-0368.yml true 0.02 0.02 ws10 QF_NRA_meti-tarski__atan__vega__3_atan-vega-3-chunk-0547.yml true 0.02 0.02 tc04 QF_NRA_meti-tarski__cbrt__3__weak_cbrt-problem-3-weak-chunk-0062.yml true 0.01 0.01 ws10 QF_NRA_meti-tarski__cbrt__3__weak_cbrt-problem-3-weak-chunk-0090.yml true 0.02 0.02 ws10 QF_NRA_meti-tarski__polypaver__bench-sqrt-3d_polypaver-bench-sqrt-3d-chunk-0442.yml true 0.02 0.02 ws10 QF_NRA_meti-tarski__sqrt__1mcosq__7_sqrt-1mcosq-7-chunk-0178.yml true 0.04 0.04 tc07 QF_NRA_meti-tarski__sqrt__1mcosq__8_sqrt-1mcosq-8-chunk-0699.yml true 0.01 0.01 tc05 --------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 72.56 - Statistics: 20 Files correct: 16 correct true: 16 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4