Error when reading proof

[AFellner]

When reading the proof QF_IDL\sep\hardware\cache_neg.2step.smt2, I get the following error:

[debug] Thread run-main exited.
[debug] Interrupting remaining threads (should be all daemons).
[debug] Sandboxed run complete..
java.lang.RuntimeException: Nonzero exit code: 1
at scala.sys.package$.error(package.scala:27)
at sbt.BuildCommon$$anonfun$toError$1.apply(Defaults.scala:1356)
at sbt.BuildCommon$$anonfun$toError$1.apply(Defaults.scala:1356)
at scala.Option.foreach(Option.scala:197)
at sbt.BuildCommon$class.toError(Defaults.scala:1356)
at sbt.package$.toError(package.scala:4)
at sbt.BuildExtra$$anonfun$fullRunInputTask$1$$anonfun$apply$64$$anonfun$apply$65.apply(Defaults.scala:1316)
at sbt.BuildExtra$$anonfun$fullRunInputTask$1$$anonfun$apply$64$$anonfun$apply$65.apply(Defaults.scala:1315)
at scala.Function1$$anonfun$compose$1.apply(Function1.scala:49)
at sbt.$tilde$greater$$anonfun$$u2219$1.apply(TypeFunctions.scala:41)
at sbt.std.Transform$$anon$5.work(System.scala:71)
at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:232)
at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:232)
at sbt.ErrorHandling$.wideConvert(ErrorHandling.scala:18)
at sbt.Execute.work(Execute.scala:238)
at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:232)
at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:232)
at sbt.ConcurrentRestrictions$$anon$4$$anonfun$1.apply(ConcurrentRestrictions.scala:160)
at sbt.CompletionService$$anon$2.call(CompletionService.scala:30)
at java.util.concurrent.FutureTask$Sync.innerRun(Unknown Source)
at java.util.concurrent.FutureTask.run(Unknown Source)
at java.util.concurrent.Executors$RunnableAdapter.call(Unknown Source)
at java.util.concurrent.FutureTask$Sync.innerRun(Unknown Source)
at java.util.concurrent.FutureTask.run(Unknown Source)
at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(Unknown Source)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(Unknown Source)
at java.lang.Thread.run(Unknown Source)
error Nonzero exit code: 1

[ceilican]

On this proof, I get a stackoverflow error, even with a very large stack size.

> compress -d examples/proofs/VeriT/ cache_neg.2step.smt2 -f skeptik
[info] Running at.logic.skeptik.ProofCompressionCLI -d examples/proofs/VeriT/ cache_neg.2step.smt2 -f skeptik
[error] Picked up JAVA_TOOL_OPTIONS: -Dfile.encoding=UTF-8 -Xmx512m -Xss512m -XX:MaxPermSize=256m
[info] 
[error] java.lang.StackOverflowError
[error]     at scala.util.parsing.combinator.RegexParsers$class.handleWhiteSpace(RegexParsers.scala:74)
[error]     at at.logic.skeptik.parser.ProofParser.handleWhiteSpace(ProofParser.scala:9)
[error]     at scala.util.parsing.combinator.RegexParsers$$anon$1.apply(RegexParsers.scala:87)
[error]     at scala.util.parsing.combinator.Parsers$Parser$$anonfun$flatMap$1.apply(Parsers.scala:239)
[error]     at scala.util.parsing.combinator.Parsers$Parser$$anonfun$flatMap$1.apply(Parsers.scala:239)
[error]     at scala.util.parsing.combinator.Parsers$$anon$3.apply(Parsers.scala:222)
[error]     at scala.util.parsing.combinator.Parsers$Parser$$anonfun$map$1.apply(Parsers.scala:242)
[error]     at scala.util.parsing.combinator.Parsers$Parser$$anonfun$map$1.apply(Parsers.scala:242)
[error]     at scala.util.parsing.combinator.Parsers$$anon$3.apply(Parsers.scala:222)
...
..
.

[ceilican]

This suggests that the combinator parser is recursing too deeply to parse a formula in this proof.

Either the formula is too deep and requires the parser too recurse so deeply (unlikely, given that I was using a very large stack size) or there is a bug in the parser that is making it recurse more than it should.

[ceilican]

Andreas: does this occur only in this proof? Or also in other proofs?

[AFellner]

As far as I can remember, this is the only proof that I used, where this error occured.