Karlheinz Friedberger

The model evaluation is directly forwarded to MathSAT: https://github.com/sosy-lab/java-smt/blob/master/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Model.java#L138 We can of course ask the MathSAT developer for internal details and potential perfomance improvements, but we would need to provide...

Hi @ThomasHaas. In my tests, based on the provided SMTLIB file, I could produce some statistics. I parsed the given file into two queries, checked satisfiability and the evaluated symbols...

Current status: - I asked Alberto (MathSAT developer) about this and still got no answer whether the model access can be optimized. - I could not yet reproduce this problem...

Thanks for checking the Buildbot tables. This should really be done from time to time. :-) I don't think that this is a bug in the wrapper, but more a...

It seems as if we mixed up two different issues here: - a segmentation fault: this is a clear bug and we should aim to fix it or report in...

As the SegFault does not appear that often, it has a minor priority. Instead of manually tracking down every call, one could dump all native calls as part of the...

Exporting is not the problem, because that is just a String representation. However, parsing such a query will (hopefully) always result in a crash.

The implementation can be found in the branch https://github.com/sosy-lab/java-smt/tree/interaction_performance

Info: The PR for SMTInterpol is here: https://github.com/ultimate-pa/smtinterpol/pull/127 (merged on 2021-07-19)

JavaSMT currently has no way to pass additional parameters to Z3. However, we already plan a new release soon (with the latest Z3, updated some days ago) and this looks...