Incompatibility with solver names #3
Description
I am trying to run PSYCO under JPF with the provided examples in order to guess how to use it. I installed all the required dependencies: jpf-core, jpf-jdart and jconstraints-z3, and the three of them work separately. I also configured the properties file so that PSYCO and its corresponding dependencies are registered as extensions. However, when I try to run one of the PSYCO examples, I get the following error message:
$ java -jar /build/RunJPF.jar /src/examples/gsoc/cev_esas/search.jpf
nov 05, 2018 3:57:41 PM gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy createSolver
WARNING: Using deprecated solver name 'NativeZ3' might fail in future releases
Exception in thread "main" java.lang.IllegalArgumentException: 'smtinterpol' does not denote a valid constraint solver (provider)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.retrieveProvider(ConstraintSolverFactory.java:173)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:199)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:225)
at gov.nasa.jpf.psyco.Psyco.run(Psyco.java:75)
at gov.nasa.jpf.psyco.Psyco.start(Psyco.java:61)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:108)
Which may be the reason for this error? And how could it be avoided?
In case the problem may reside in the configuration site.properties file, I attach the contents of mine:
JPF site configuration
jpf-core =
jpf-jdart =
jconstraints =
jconstraints-z3 =
psyco =
extensions = ${jpf-core}:${psyco}:${jconstraints}:${jconstraints-z3}
Note that jpf-jdart is not included among the extensions because its installation instructions explicitly keep it out.
Thanks in advance and sorry for the inconveniencies.