# .

* SAT 0
* UNSAT 0
* TIMEOUT 0
* UNKNOWN 0

* UNSET 57

* ERROR 57

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: AUFBVFP.tar.zst
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: bc6c38e7d3424b88a505cacba4b268d0774d4547
Z3 branch: master
Z3 options: "-T:20"
Z3 inputs: https://zenodo.org/records/16740866/files/AUFBVFP.tar.zst?download=1
Z3 commit message: [code-simplifier] Simplify `api_ast.cpp` by removing unreachable branch and stray comment (#9570)

This change simplifies recently touched API code in
`src/api/api_ast.cpp` without altering semantics. It removes an
unreachable error path in `Z3_get_index_value` and deletes an empty
comment in `Z3_mk_rec_func_decl`.

- **`Z3_get_index_value`: remove dead branch**
- After validating `a` is non-null and of kind `AST_VAR`, the conversion
to `var*` is already guaranteed by existing AST casting invariants.
- The redundant null-check/error-return branch was removed, leaving a
direct index return.

- **`Z3_mk_rec_func_decl`: remove noise**
  - Deleted a stray empty `//` line.

```cpp
// before
var* va = to_var(_a);
if (va) {
    return va->get_idx();
}
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;

// after
var* va = to_var(_a);
return va->get_idx();
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|non-incremental/AUFBVFP/20210301-Alive2/ph7/611_ph7.smt2     | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/ph7/757_ph7.smt2     | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/ph7/568_ph7.smt2     | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/bzip2/001_bzip2.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/sqlite3/892_sqlite3.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/sqlite3/917_sqlite3.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/305_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/358_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/277_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/300_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/457_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/322_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/290_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/430_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/409_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/453_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/293_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/455_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/410_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/369_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/288_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/342_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/459_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/434_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/392_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/397_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/356_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/343_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/385_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/426_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/354_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/340_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/368_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/422_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/445_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/461_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/295_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/411_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/446_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/449_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/324_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/303_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2/oggenc/344_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/744_ph7.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/583_ph7.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/489_ph7.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/sqlite3/870_sqlite3.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/sqlite3/816_sqlite3.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/346_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/351_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/357_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/386_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/374_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/392_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/384_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/352_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |
|non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/344_oggenc.smt2 | 1000.000s | -1B| unset | -1 |  |  |