BENCHMARK INFORMATION benchmark definition: run_definitions/opensmt_inc_QF_LinearIntArith.xml name: opensmt_inc_QF_LinearIntArith run sets: OpenSMT,0,Incremental.task date: Mon, 2025-06-23 15:05:28 CEST tool: OpenSMT tool executable: ./unpack/ef2e8e3315254aac78ddc31cdf6813a5640ea2cb5bc2c7901a270d8285b95c79/opensmt 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 ------------------------------------------------------------ OpenSMT,0,Incremental.task Run set 1 of 1 with options 'unpack/ef2e8e3315254aac78ddc31cdf6813a5640ea2cb5bc2c7901a270d8285b95c79/opensmt' and propertyfile 'benchmarks/properties/SMT.prp' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------------------- QF_LIA_UltimateBuchiAutomizer_AliasDarteFeautrierGonnord-SAS2010-loops_true-termination.c.yml TIMEOUT (TIMEOUT (15856 correct)) 61.09 61.00 tc01 QF_LIA_UltimateBuchiAutomizer_GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c.yml TIMEOUT (TIMEOUT (14182 correct)) 61.49 61.00 ws14 QF_LIA_kratos_systemC_swmc_mem_slave_tlm.5.c.kratos.int.bmc_k100.yml TIMEOUT (TIMEOUT (35 correct)) 61.04 61.00 tc01 QF_LIA_kratos_systemC_swmc_pc_sfifo_3.c.kratos.int.ind_k100.yml TIMEOUT (TIMEOUT (41 correct)) 61.01 61.00 tc01 QF_LIA_kratos_systemC_swmc_pipeline-bug.c.kratos.int.bmc_k100.yml TIMEOUT (TIMEOUT (51 correct)) 61.03 61.00 tc02 QF_LIA_kratos_systemC_swmc_pipeline-bug.c.kratos.int.ind_k100.yml TIMEOUT (TIMEOUT (31 correct)) 61.03 61.00 tc08 QF_LIA_kratos_systemC_swmc_transmitter.10.c.kratos.int.bmc_k100.yml TIMEOUT (TIMEOUT (17 correct)) 61.18 61.00 tc02 QF_LIA_lustre_DRAGON_all.bmc_k100.yml TIMEOUT (TIMEOUT (51 correct)) 61.01 61.00 tc02 QF_LIA_lustre_MESI_all.bmc_k100.yml DONE (101 correct) 44.00 44.00 tc03 QF_LIA_lustre_MESI_all.ind_k100.yml TIMEOUT (TIMEOUT (162 correct)) 61.04 61.00 tc03 QF_LIA_lustre_SYNAPSE_all.bmc_k100.yml DONE (101 correct) 17.91 17.91 tc08 QF_LIA_lustre_durationThm_1.ind_k100.yml TIMEOUT (TIMEOUT (113 correct)) 61.01 61.00 tc06 QF_LIA_lustre_rtp_all.ind_k100.yml TIMEOUT (TIMEOUT (126 correct)) 61.03 61.00 tc06 QF_LIA_lustre_rtp_vt.bmc_k100.yml TIMEOUT (TIMEOUT (38 correct)) 61.01 61.00 tc03 QF_LIA_lustre_speed2.ind_k100.yml DONE (202 correct) 4.16 4.16 tc02 QF_LIA_lustre_two_counters.ind_k100.yml DONE (202 correct) 4.06 4.06 tc07 QF_LIA_ultimateAutomizer_Problem05_00_false-unreach-call.c.yml TIMEOUT (TIMEOUT (1293 correct)) 61.02 61.00 tc07 QF_LIA_ultimateAutomizer_Problem09_50_true-unreach-call.c.yml TIMEOUT (TIMEOUT (998 correct)) 61.02 61.00 tc05 QF_LIA_ultimateAutomizer_toy2_false-unreach-call_false-termination.cil.c.yml TIMEOUT (TIMEOUT (4411 correct)) 61.02 61.00 tc02 QF_LIA_ultimateKojak_kundu_true-unreach-call_false-termination.cil.c.prep.yml TIMEOUT (TIMEOUT (20451 correct)) 61.02 61.00 tc08 -------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 75.09 - Statistics: 20 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 20