# . * SAT 0 * UNSAT 2 * TIMEOUT 43 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for cvc5
-
Job description: 
Job tag: CVC5-threads-1-mode-sequential-smtcomp2025-QF_IDL-timeout20min
Runner: rise-runner-2
cvc5 repo: cvc5/cvc5
cvc5 commit: e7e5bb6ea37ae6122da5c4f165b73c87089be765
cvc5 branch: main
cvc5 mode: sequential
cvc5 portfolio mode: graduated
cvc5 portfolio strategies: "decision-scatter decision-cube"
cvc5 partition budget: 1
cvc5 partitioning options: "--partition-when=tlimit --partition-start-time=3 --partition-time-interval=0.1 --partition-check=standard"
cvc5 portfolio options: ""
cvc5 solver options: ""
cvc5 solver jobs: 1
cvc5 timeout: 1200
cvc5 inputs: inputs/smt_comp_2025_parallel/QF_IDL
cvc5 commit message: Alethe add INTS_LOG2 and INTS_ISPOW2 (#12626)

These two operators do appear in the proofs of bit-vector benchmarks.

Co-authored-by: Haniel Barbosa
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled96514.smt2 | 597.201s | 444.0MiB| unsat | 0 | | | |scrambled89071.smt2 | 1177.411s | 574.0MiB| unsat | 0 | | | |scrambled1379.smt2 | 1200.042s | 228.0MiB| timeout | 0 | | | |scrambled119992.smt2 | 1200.043s | 233.0MiB| timeout | 0 | | | |scrambled23483.smt2 | 1200.043s | 194.0MiB| timeout | 0 | | | |scrambled96733.smt2 | 1200.045s | 207.0MiB| timeout | 0 | | | |scrambled116992.smt2 | 1200.047s | 266.0MiB| timeout | 0 | | | |scrambled62536.smt2 | 1200.048s | 302.0MiB| timeout | 0 | | | |scrambled35345.smt2 | 1200.049s | 316.0MiB| timeout | 0 | | | |scrambled75206.smt2 | 1200.050s | 271.0MiB| timeout | 0 | | | |scrambled97138.smt2 | 1200.059s | 364.0MiB| timeout | 0 | | | |scrambled100416.smt2 | 1200.064s | 430.0MiB| timeout | 0 | | | |scrambled41801.smt2 | 1200.065s | 219.0MiB| timeout | 0 | | | |scrambled9927.smt2 | 1200.082s | 569.0MiB| timeout | 0 | | | |scrambled1447.smt2 | 1200.090s | 397.0MiB| timeout | 0 | | | |scrambled124624.smt2 | 1200.090s | 696.0MiB| timeout | 0 | | | |scrambled103851.smt2 | 1200.090s | 409.0MiB| timeout | 0 | | | |scrambled41773.smt2 | 1200.092s | 270.0MiB| timeout | 0 | | | |scrambled41312.smt2 | 1200.093s | 270.0MiB| timeout | 0 | | | |scrambled15284.smt2 | 1200.094s | 293.0MiB| timeout | 0 | | | |scrambled27577.smt2 | 1200.095s | 282.0MiB| timeout | 0 | | | |scrambled62810.smt2 | 1200.099s | 325.0MiB| timeout | 0 | | | |scrambled38610.smt2 | 1200.105s | 365.0MiB| timeout | 0 | | | |scrambled42287.smt2 | 1200.107s | 354.0MiB| timeout | 0 | | | |scrambled6373.smt2 | 1200.109s | 369.0MiB| timeout | 0 | | | |scrambled14967.smt2 | 1200.110s | 509.0MiB| timeout | 0 | | | |scrambled78606.smt2 | 1200.115s | 569.0MiB| timeout | 0 | | | |scrambled79181.smt2 | 1200.118s | 451.0MiB| timeout | 0 | | | |scrambled98799.smt2 | 1200.118s | 622.0MiB| timeout | 0 | | | |scrambled122413.smt2 | 1200.122s | 480.0MiB| timeout | 0 | | | |scrambled4441.smt2 | 1200.122s | 652.0MiB| timeout | 0 | | | |scrambled62859.smt2 | 1200.124s | 427.0MiB| timeout | 0 | | | |scrambled21544.smt2 | 1200.125s | 491.0MiB| timeout | 0 | | | |scrambled78432.smt2 | 1200.127s | 531.0MiB| timeout | 0 | | | |scrambled58720.smt2 | 1200.130s | 591.0MiB| timeout | 0 | | | |scrambled128361.smt2 | 1200.135s | 609.0MiB| timeout | 0 | | | |scrambled54073.smt2 | 1200.136s | 573.0MiB| timeout | 0 | | | |scrambled82743.smt2 | 1200.139s | 628.0MiB| timeout | 0 | | | |scrambled117178.smt2 | 1200.140s | 957.0MiB| timeout | 0 | | | |scrambled90733.smt2 | 1200.145s | 688.0MiB| timeout | 0 | | | |scrambled92133.smt2 | 1200.175s | 992.0MiB| timeout | 0 | | | |scrambled122058.smt2 | 1200.179s | 1204.0MiB| timeout | 0 | | | |scrambled109208.smt2 | 1200.205s | 1369.0MiB| timeout | 0 | | | |scrambled15552.smt2 | 1200.209s | 1400.0MiB| timeout | 0 | | | |scrambled25140.smt2 | 1201.036s | 10.848GiB| timeout | 0 | | |