Re: [Smtcomp-discussion] a day to go

[Tjark W. <tja...@it...>]

David, Aaron,

I can run jobs now. The problem may have been caused by me specifying
invalid input for the seed value before. (If this is indeed the case,
http 500 is not the most helpful error message.)

Aaron -- the seed value is disregarded by the "SMT-COMP 2014 Scrambler"
pre-processor. This is expected, as our current pre-processor script is
only passing $1 (i.e., the name of the benchmark file) to the actual
scrambler. How exactly is the job's seed value supplied to the
pre-processor? (The user manual appears silent about this, which is
understandable, of course.)

Aaron -- it appears that the "solver summary" still counts
starexec-unknown as a wrong result. (I suppose this is a known issue.
In any case, it is not critical.)

David -- I am afraid I failed to wrap the latest nightly build of Z3
for StarExec. I tried to supply all needed libraries but only got to a
point where there is no output from the solver at all (rather than an
error message), which makes further debugging tricky. Since (1) Z3 is
running non-competitively anyway and (2) it appears that there has not
been an official (stable) release of Z3 since 2012, I suggest we simply
run the SMT-EVAL-2013 version of Z3 again for comparison. I have linked
this version to the Solvers-Preliminary space.

Best,
Tjark