# . * SAT 0 * UNSAT 0 * TIMEOUT 0 * UNKNOWN 57 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/AUFBVFP.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-AUFBVFP.tar.zst-do
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 459629c662eb7abf25a010b7383431a9f729d234
Z3 branch: master
Z3 options: "-T:20 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify sls-smt)" model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/AUFBVFP.tar.zst?download=1
Z3 commit message: bugfixes to ho_matcher

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/AUFBVFP/20210301-Alive2/oggenc/358_oggenc.smt2 | 0.034s | 20.22MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/368_oggenc.smt2 | 0.039s | 20.968MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/290_oggenc.smt2 | 0.040s | 20.816MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/346_oggenc.smt2 | 0.040s | 21.112MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/322_oggenc.smt2 | 0.046s | 20.816MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/357_oggenc.smt2 | 0.046s | 20.62MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/449_oggenc.smt2 | 0.047s | 21.044MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/ph7/611_ph7.smt2 | 0.048s | 21.18MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/411_oggenc.smt2 | 0.049s | 20.192MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/340_oggenc.smt2 | 0.049s | 19.888MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/392_oggenc.smt2 | 0.050s | 20.028MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/354_oggenc.smt2 | 0.050s | 21.024MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/295_oggenc.smt2 | 0.051s | 21.316MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/303_oggenc.smt2 | 0.052s | 20.616MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/293_oggenc.smt2 | 0.054s | 20.52MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/409_oggenc.smt2 | 0.055s | 20.176MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/459_oggenc.smt2 | 0.056s | 20.476MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/343_oggenc.smt2 | 0.056s | 20.48MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/583_ph7.smt2 | 0.056s | 20.308MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/455_oggenc.smt2 | 0.057s | 20.304MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/489_ph7.smt2 | 0.060s | 21.6MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/288_oggenc.smt2 | 0.062s | 20.924MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/sqlite3/917_sqlite3.smt2 | 0.064s | 21.14MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/392_oggenc.smt2 | 0.066s | 21.252MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/410_oggenc.smt2 | 0.068s | 21.328MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/351_oggenc.smt2 | 0.068s | 21.624MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/374_oggenc.smt2 | 0.069s | 21.272MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/342_oggenc.smt2 | 0.070s | 21.108MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/384_oggenc.smt2 | 0.070s | 20.972MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/305_oggenc.smt2 | 0.073s | 20.928MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/344_oggenc.smt2 | 0.073s | 20.152MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/324_oggenc.smt2 | 0.076s | 21.464MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/bzip2/001_bzip2.smt2 | 0.077s | 21.844MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/369_oggenc.smt2 | 0.078s | 21.924MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/426_oggenc.smt2 | 0.082s | 22.036MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/344_oggenc.smt2 | 0.085s | 22.26MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/397_oggenc.smt2 | 0.086s | 22.284MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/422_oggenc.smt2 | 0.086s | 21.608MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/sqlite3/870_sqlite3.smt2 | 0.087s | 22.392MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/434_oggenc.smt2 | 0.089s | 21.292MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/356_oggenc.smt2 | 0.092s | 21.404MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/277_oggenc.smt2 | 0.102s | 20.504MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/sqlite3/892_sqlite3.smt2 | 0.111s | 22.024MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/445_oggenc.smt2 | 0.130s | 21.144MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/744_ph7.smt2 | 0.143s | 23.196MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/sqlite3/816_sqlite3.smt2 | 0.167s | 24.2MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/ph7/568_ph7.smt2 | 0.177s | 23.428MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/457_oggenc.smt2 | 0.183s | 23.48MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/ph7/757_ph7.smt2 | 0.190s | 23.324MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/352_oggenc.smt2 | 0.217s | 27.98MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/430_oggenc.smt2 | 0.267s | 25.292MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/385_oggenc.smt2 | 0.374s | 72.752MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/453_oggenc.smt2 | 0.418s | 72.94MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/461_oggenc.smt2 | 0.586s | 72.98MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/300_oggenc.smt2 | 0.619s | 38.78MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/446_oggenc.smt2 | 0.780s | 48.444MiB| unknown | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/386_oggenc.smt2 | 2.096s | 262.0MiB| unknown | 0 | | |