skeptik -a RP -a (D*RPI*LU) -f smt2 examples/proofs/VeriT/eq_diamond9.smt2
as instructed in the README file results in an exception's being thrown:
java.lang.Exception: Failure: `)' expected but `*' found
at at.logic.skeptik.parser.AlgorithmParser$.parse(AlgorithmParser.scala:34)
[...]
Upon a short investigation, I was led to conclude that the exception has to do with a modification of AlgorithmParser.scala (6fb9ce6, specifically) and thus all that is required is to update the README example command so that it reflects the fact that when a composed algorithm is passed as an argument on the command line, a dash ('-') instead of an asterisk ('*') should be used as the delimiter.
ceilican
commented
10 years ago
Hello there, executing the command
skeptik -a RP -a (D*RPI*LU) -f smt2 examples/proofs/VeriT/eq_diamond9.smt2as instructed in the README file results in an exception's being thrown:
Upon a short investigation, I was led to conclude that the exception has to do with a modification of
AlgorithmParser.scala(6fb9ce6, specifically) and thus all that is required is to update the README example command so that it reflects the fact that when a composed algorithm is passed as an argument on the command line, a dash ('-') instead of an asterisk ('*') should be used as the delimiter.Cheers, Andrej