BENCHMARK INFORMATION benchmark definition: run_definitions/yices2_inc_QF_LinearIntArith.xml name: yices2_inc_QF_LinearIntArith run sets: Yices2,3,Incremental.task date: Mon, 2025-06-23 15:39:50 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,3,Incremental.task Run set 1 of 1 with options 'unpack/9a71a8be5336a24d9219bd7598075f7ba06f85484bb819f3e8992e68a0a0d6cd/yices_smt2 --incremental' and propertyfile 'benchmarks/properties/SMT.prp' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------------------- QF_LIA_UltimateBuchiAutomizer_AliasDarteFeautrierGonnord-SAS2010-loops_true-termination.c.yml DONE (54536 correct) 7.70 7.51 tc02 QF_LIA_UltimateBuchiAutomizer_GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c.yml DONE (30044 correct) 15.96 15.58 tc02 QF_LIA_kratos_systemC_swmc_mem_slave_tlm.5.c.kratos.int.bmc_k100.yml TIMEOUT (TIMEOUT (48 correct)) 61.03 61.00 tc08 QF_LIA_kratos_systemC_swmc_pc_sfifo_3.c.kratos.int.ind_k100.yml TIMEOUT (TIMEOUT (129 correct)) 61.05 61.00 tc08 QF_LIA_kratos_systemC_swmc_pipeline-bug.c.kratos.int.bmc_k100.yml TIMEOUT (TIMEOUT (62 correct)) 61.03 61.00 tc05 QF_LIA_kratos_systemC_swmc_pipeline-bug.c.kratos.int.ind_k100.yml TIMEOUT (TIMEOUT (89 correct)) 61.06 61.00 tc02 QF_LIA_kratos_systemC_swmc_transmitter.10.c.kratos.int.bmc_k100.yml TIMEOUT (TIMEOUT (41 correct)) 61.17 61.00 tc08 QF_LIA_lustre_DRAGON_all.bmc_k100.yml TIMEOUT (TIMEOUT (45 correct)) 61.00 61.00 tc02 QF_LIA_lustre_MESI_all.bmc_k100.yml TIMEOUT (TIMEOUT (74 correct)) 61.00 61.00 tc08 QF_LIA_lustre_MESI_all.ind_k100.yml TIMEOUT (TIMEOUT (138 correct)) 60.99 61.00 tc02 QF_LIA_lustre_SYNAPSE_all.bmc_k100.yml DONE (101 correct) 53.25 53.25 tc05 QF_LIA_lustre_durationThm_1.ind_k100.yml TIMEOUT (TIMEOUT (192 correct)) 61.00 61.00 tc08 QF_LIA_lustre_rtp_all.ind_k100.yml TIMEOUT (TIMEOUT (136 correct)) 61.01 61.00 tc02 QF_LIA_lustre_rtp_vt.bmc_k100.yml TIMEOUT (TIMEOUT (32 correct)) 61.00 61.00 tc02 QF_LIA_lustre_speed2.ind_k100.yml DONE (202 correct) 0.94 0.94 tc02 QF_LIA_lustre_two_counters.ind_k100.yml DONE (202 correct) 0.19 0.20 tc05 QF_LIA_ultimateAutomizer_Problem05_00_false-unreach-call.c.yml TIMEOUT (TIMEOUT (469055 correct)) 62.46 61.00 tc08 QF_LIA_ultimateAutomizer_Problem09_50_true-unreach-call.c.yml TIMEOUT (TIMEOUT (278952 correct)) 62.42 61.00 tc05 QF_LIA_ultimateAutomizer_toy2_false-unreach-call_false-termination.cil.c.yml DONE (201788 correct) 27.15 26.52 tc08 QF_LIA_ultimateKojak_kundu_true-unreach-call_false-termination.cil.c.prep.yml TIMEOUT (TIMEOUT (561671 correct)) 62.47 61.00 tc08 -------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 71.60 - Statistics: 20 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 20