# . * SAT 2 * UNSAT 55 * TIMEOUT 11 * UNKNOWN 0 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/UFIDL.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-UFIDL.tar.zst-down
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 459629c662eb7abf25a010b7383431a9f729d234
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/UFIDL.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/UFIDL/boogie/UnreachableBlocks_R-vc_nested.smt2 | 0.024s | 19.524MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/UnreachableBlocks_Q-vc_nested.smt2 | 0.025s | 19.788MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/FormulaTerm_less-noinfer_2.smt2 | 0.025s | 20.112MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns8.smt2 | 0.026s | 20.36MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns3.smt2 | 0.027s | 20.364MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns4.smt2 | 0.028s | 20.88MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/Arrays_P1-noinfer.smt2 | 0.028s | 20.416MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns9.smt2 | 0.030s | 21.136MiB| unsat | 0 | | | |non-incremental/UFIDL/sledgehammer/QEpres/smtlib.858843.smt2 | 0.031s | 21.072MiB| sat | 0 | | | |non-incremental/UFIDL/sledgehammer/QEpres/smtlib.858765.smt2 | 0.031s | 20.284MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala0.smt2 | 0.031s | 20.624MiB| unsat | 0 | | | |non-incremental/UFIDL/sledgehammer/QEpres/smtlib.858929.smt2 | 0.035s | 20.14MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala9.smt2 | 0.036s | 20.652MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns0.smt2 | 0.036s | 20.424MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/equiv3_M-infer_e-vc_local.smt2 | 0.037s | 20.092MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns1.smt2 | 0.038s | 20.312MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala4.smt2 | 0.042s | 20.62MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns13.smt2 | 0.043s | 21.116MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala6.smt2 | 0.047s | 21.556MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/FormulaTerm_LESS-noinfer_3.smt2 | 0.050s | 20.384MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala5.smt2 | 0.057s | 21.688MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/Call_DifferentFormalNames-noinfer.smt2 | 0.057s | 19.596MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/False_Test1-noinfer.smt2 | 0.057s | 19.592MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/Passification_Loop-noinfer.smt2 | 0.058s | 19.628MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/AssumeEnsures_Caller0-noinfer.smt2 | 0.058s | 19.708MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/Call_DifferentFormalNames-noinfer_1.smt2 | 0.058s | 19.752MiB| unsat | 0 | | | |non-incremental/UFIDL/sledgehammer/QEpres/smtlib.858852.smt2 | 0.059s | 20.94MiB| sat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala2.smt2 | 0.059s | 21.644MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/Arrays_Skip0-noinfer.smt2 | 0.059s | 19.592MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/False_Test2-noinfer.smt2 | 0.059s | 20.34MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/UnreachableBlocks_P-vc_nested.smt2 | 0.059s | 19.844MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/heapsucc0_M-infer_eh-vc_local.smt2 | 0.059s | 19.872MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/heapsucc1_M-infer_eh-vc_local.smt2 | 0.059s | 19.868MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/Passification_UnreachableBlock-noinfer.smt2 | 0.060s | 19.672MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/FormulaTerm_less-noinfer_1.smt2 | 0.060s | 19.596MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/equiv2_M-infer_e-vc_local.smt2 | 0.060s | 19.816MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/loop0_M-infer_e-vc_local.smt2 | 0.062s | 19.588MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns7.smt2 | 0.063s | 20.62MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns2.smt2 | 0.063s | 20.552MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns11.smt2 | 0.063s | 20.356MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/NestedVC_P-vc_nested.smt2 | 0.063s | 19.704MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns12.smt2 | 0.064s | 20.34MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/Old_SwapElems-noinfer.smt2 | 0.065s | 20.7MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/Arrays_Q1-noinfer.smt2 | 0.065s | 20.368MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala3.smt2 | 0.066s | 20.732MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala10.smt2 | 0.067s | 20.656MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns6.smt2 | 0.067s | 21.368MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/Arrays_Skip1-noinfer.smt2 | 0.067s | 20.288MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala13.smt2 | 0.068s | 21.384MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns5.smt2 | 0.068s | 20.568MiB| unsat | 0 | | | |non-incremental/UFIDL/Burns/burns10.smt2 | 0.068s | 21.116MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/FormulaTerm_or-noinfer.smt2 | 0.069s | 20.636MiB| unsat | 0 | | | |non-incremental/UFIDL/sledgehammer/TypeSafe/smtlib.675311.smt2 | 0.070s | 20.104MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala7.smt2 | 0.073s | 21.644MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala12.smt2 | 0.079s | 21.672MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala8.smt2 | 0.086s | 21.652MiB| unsat | 0 | | | |non-incremental/UFIDL/RicartAgrawala/ricart-agrawala11.smt2 | 0.094s | 22.16MiB| unsat | 0 | | | |non-incremental/UFIDL/boogie/Call_DifferentFormalNames-noinfer_3.smt2 | 20.029s | 228.0MiB| timeout | 0 | | | |non-incremental/UFIDL/boogie/Call_DifferentFormalNames-noinfer_2.smt2 | 20.063s | 230.0MiB| timeout | 0 | | | |non-incremental/UFIDL/boogie/NestedVC_Q-vc_nested.smt2 | 20.067s | 225.0MiB| timeout | 0 | | | |non-incremental/UFIDL/boogie/Call_Foo-noinfer.smt2 | 20.068s | 229.0MiB| timeout | 0 | | | |non-incremental/UFIDL/sledgehammer/TypeSafe/smtlib.683530.smt2 | 20.303s | 2761.0MiB| timeout | 0 | | | |non-incremental/UFIDL/sledgehammer/TypeSafe/smtlib.697341.smt2 | 20.308s | 2919.0MiB| timeout | 0 | | | |non-incremental/UFIDL/sledgehammer/TypeSafe/smtlib.968906.smt2 | 20.414s | 4049.0MiB| timeout | 0 | | | |non-incremental/UFIDL/sledgehammer/TypeSafe/smtlib.962381.smt2 | 20.421s | 4087.0MiB| timeout | 0 | | | |non-incremental/UFIDL/sledgehammer/TypeSafe/smtlib.976292.smt2 | 20.450s | 4095.0MiB| timeout | 0 | | | |non-incremental/UFIDL/sledgehammer/TypeSafe/smtlib.976791.smt2 | 20.499s | 4077.0MiB| timeout | 0 | | | |non-incremental/UFIDL/sledgehammer/Fundamental_Theorem_Algebra/smtlib.1308248.smt2 | 20.636s | 4923.0MiB| timeout | 0 | | |