Karlheinz Friedberger
Karlheinz Friedberger
Thanks for your patience. I do not yet have a positive message for @ThomasHaas. This is just a intermediate report. Well, the option handling in Z3 is worse than expected....
The problem might be caused by Scala (from Princess) and memory shortage. Maybe the used Scala version does not (always) work with the installed JVM version. I will take a...
I am unable to reproduce the problem on my local system. However, I can provide a few more details, from logs or related Java-issues: 1) The failing build on WIndows...
This issue is quite high on my list, however it has not yet reached the top level. :smiley: The CI does not always fail, but we had a failing JUnit...
It is actually an interesting question which solvers do have support for wich argument types. At least `Integer` is supported by all solvers.
The same problem still appears with OptiMathSAT 1.7.3.
Thank you for your interest in JavaSMT. We will take a look soon and report back. An example setup for Gradle would be a great idea to extend our documentation.
Is there anything left to do? Otherwise we could merge this and apply potential fixes later.
You can use a natively-installed version of Z3. JavaSMT needs to find the JAR-file for Z3, i.e., you need provide Z3 (in form of a JAR and a native library)...
JavaSMT does not provide a way to use process- or pipe-based interaction with SMT solvers (which seems to be your intent), but only provides interaction via native APIs. This was...