# .

* SAT 0
* UNSAT 2
* TIMEOUT 43
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for cvc5
-
Job description: 
Job tag: CVC5-threads-8-mode-partition-smtcomp2025-QF_IDL-timeout20min
Runner: rise-runner-2
cvc5 repo: cvc5/cvc5
cvc5 commit: e7e5bb6ea37ae6122da5c4f165b73c87089be765
cvc5 branch: main
cvc5 mode: partition
cvc5 portfolio mode: graduated
cvc5 portfolio strategies: "decision-scatter decision-cube"
cvc5 partition budget: 8
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: 8
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 <hanielbbarbosa@gmail.com>

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|scrambled96514.smt2                                          | 1121.113s | 988.0MiB| unsat | 0 |  |  |
|scrambled89071.smt2                                          | 1189.366s | 2252.0MiB| unsat | 0 |  |  |
|scrambled96733.smt2                                          | 1199.677s | 1564.0MiB| timeout | 0 |  |  |
|scrambled6373.smt2                                           | 1199.698s | 2623.0MiB| timeout | 0 |  |  |
|scrambled122058.smt2                                         | 1199.714s | 9151.0MiB| timeout | 0 |  |  |
|scrambled62810.smt2                                          | 1199.729s | 2411.0MiB| timeout | 0 |  |  |
|scrambled21544.smt2                                          | 1199.777s | 2718.0MiB| timeout | 0 |  |  |
|scrambled27577.smt2                                          | 1199.782s | 3585.0MiB| timeout | 0 |  |  |
|scrambled82743.smt2                                          | 1199.817s | 1752.0MiB| timeout | 0 |  |  |
|scrambled23483.smt2                                          | 1199.840s | 1448.0MiB| timeout | 0 |  |  |
|scrambled1447.smt2                                           | 1199.850s | 2136.0MiB| timeout | 0 |  |  |
|scrambled97138.smt2                                          | 1199.856s | 2746.0MiB| timeout | 0 |  |  |
|scrambled41773.smt2                                          | 1199.863s | 1789.0MiB| timeout | 0 |  |  |
|scrambled103851.smt2                                         | 1199.871s | 3086.0MiB| timeout | 0 |  |  |
|scrambled9927.smt2                                           | 1199.882s | 1452.0MiB| timeout | 0 |  |  |
|scrambled14967.smt2                                          | 1199.895s | 3514.0MiB| timeout | 0 |  |  |
|scrambled75206.smt2                                          | 1199.895s | 1828.0MiB| timeout | 0 |  |  |
|scrambled42287.smt2                                          | 1199.896s | 2585.0MiB| timeout | 0 |  |  |
|scrambled15284.smt2                                          | 1199.901s | 1782.0MiB| timeout | 0 |  |  |
|scrambled92133.smt2                                          | 1199.911s | 7502.0MiB| timeout | 0 |  |  |
|scrambled78606.smt2                                          | 1199.919s | 1467.0MiB| timeout | 0 |  |  |
|scrambled4441.smt2                                           | 1199.963s | 4294.0MiB| timeout | 0 |  |  |
|scrambled79181.smt2                                          | 1199.972s | 3285.0MiB| timeout | 0 |  |  |
|scrambled62536.smt2                                          | 1199.982s | 874.0MiB| timeout | 0 |  |  |
|scrambled128361.smt2                                         | 1199.985s | 3051.0MiB| timeout | 0 |  |  |
|scrambled98799.smt2                                          | 1199.992s | 3577.0MiB| timeout | 0 |  |  |
|scrambled38610.smt2                                          | 1200.002s | 2791.0MiB| timeout | 0 |  |  |
|scrambled78432.smt2                                          | 1200.007s | 2773.0MiB| timeout | 0 |  |  |
|scrambled41312.smt2                                          | 1200.019s | 1606.0MiB| timeout | 0 |  |  |
|scrambled109208.smt2                                         | 1200.219s | 9778.0MiB| timeout | 0 |  |  |
|scrambled62859.smt2                                          | 1200.271s | 3183.0MiB| timeout | 0 |  |  |
|scrambled1379.smt2                                           | 1200.363s | 1499.0MiB| timeout | 0 |  |  |
|scrambled35345.smt2                                          | 1200.369s | 2097.0MiB| timeout | 0 |  |  |
|scrambled119992.smt2                                         | 1200.381s | 1619.0MiB| timeout | 0 |  |  |
|scrambled41801.smt2                                          | 1200.383s | 1841.0MiB| timeout | 0 |  |  |
|scrambled116992.smt2                                         | 1200.405s | 2083.0MiB| timeout | 0 |  |  |
|scrambled100416.smt2                                         | 1200.439s | 2966.0MiB| timeout | 0 |  |  |
|scrambled122413.smt2                                         | 1200.448s | 2940.0MiB| timeout | 0 |  |  |
|scrambled54073.smt2                                          | 1200.453s | 2425.0MiB| timeout | 0 |  |  |
|scrambled58720.smt2                                          | 1200.496s | 3679.0MiB| timeout | 0 |  |  |
|scrambled90733.smt2                                          | 1200.506s | 4240.0MiB| timeout | 0 |  |  |
|scrambled124624.smt2                                         | 1200.518s | 5333.0MiB| timeout | 0 |  |  |
|scrambled117178.smt2                                         | 1200.521s | 5312.0MiB| timeout | 0 |  |  |
|scrambled15552.smt2                                          | 1200.596s | 9704.0MiB| timeout | 0 |  |  |
|scrambled25140.smt2                                          | 1200.828s | 9039.0MiB| timeout | 0 |  |  |