"String index out of range: 0" in ASCIIStringEncoder

Stainless throws this exception when running the termination checker (stainless --solvers=nativez3 --termination) over this benchmark:

import stainless.lang._
import stainless.annotation._
import stainless.collection._

object index {
  val xs = List("a" -> 1, "b" -> 2, "c" -> 3, "d" -> 4)

  def test(map: Map[String, Int]) = {
    val res = xs.foldLeft(map) {
      case (acc, (k, v)) => acc.updated(k, v)
    }

    res.get("d") == Some(4)
  }.holds
}

The string it is apparently attempting unescape is: !0!

Trace: (click to expand)

``` [Internal] Error: String index out of range: 0. Trace: [Internal] - java.lang.String.charAt(String.java:658) [Internal] - inox.solvers.theories.ASCIIStringEncoder$class.inox$solvers$theories$ASCIIStringEncoder$$decodeFirstByte(ASCIIStringEncoder.scala:51) [Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:89) [Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:103) [Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:106) [Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153) [Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.immutable.List.foreach(List.scala:381) [Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234) [Internal] - scala.collection.immutable.List.map(List.scala:285) [Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152) [Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119) [Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153) [Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.immutable.List.foreach(List.scala:381) [Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234) [Internal] - scala.collection.immutable.List.map(List.scala:285) [Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152) [Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119) [Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153) [Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.immutable.List.foreach(List.scala:381) [Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234) [Internal] - scala.collection.immutable.List.map(List.scala:285) [Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152) [Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119) [Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153) [Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.immutable.List.foreach(List.scala:381) [Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234) [Internal] - scala.collection.immutable.List.map(List.scala:285) [Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152) [Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119) [Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153) [Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.immutable.List.foreach(List.scala:381) [Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234) [Internal] - scala.collection.immutable.List.map(List.scala:285) [Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152) [Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119) [Internal] - inox.ast.TreeTransformer$TreeTransformerComposition$class.transform(TreeOps.scala:274) [Internal] - inox.ast.TreeTransformer$$anon$1.transform(TreeOps.scala:293) [Internal] - inox.ast.ProgramTransformer$class.decode(ProgramOps.scala:27) [Internal] - inox.ast.ProgramTransformer$$anon$4.decode(ProgramOps.scala:46) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.decode(UnrollingSolver.scala:65) [Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.decode(SolverFactory.scala:122) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$43.apply(UnrollingSolver.scala:541) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$43.apply(UnrollingSolver.scala:541) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:179) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:179) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.immutable.Map$Map3.foreach(Map.scala:161) [Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234) [Internal] - scala.collection.AbstractTraversable.map(Traversable.scala:104) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$class.getModel(UnrollingSolver.scala:179) [Internal] - inox.solvers.z3.Z3Unrolling$ModelWrapper.getModel(Z3Unrolling.scala:66) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.inox$solvers$unrolling$AbstractUnrollingSolver$$extractTotalModel(UnrollingSolver.scala:541) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:671) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:552) [Internal] - scala.util.Try$.apply(Try.scala:192) [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93) [Internal] - inox.utils.TimerStorage.run(Timer.scala:88) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.checkAssumptions(UnrollingSolver.scala:552) [Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:122) [Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$checkAssumptions$1.apply(TimeoutSolver.scala:44) [Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$checkAssumptions$1.apply(TimeoutSolver.scala:44) [Internal] - inox.utils.TimeoutFor.interruptAfter(TimeoutFor.scala:36) [Internal] - inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:43) [Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:122) [Internal] - inox.tip.TipDebugger$class.checkAssumptions(TipDebugger.scala:61) [Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.checkAssumptions(SolverFactory.scala:122) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.check(UnrollingSolver.scala:88) [Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:122) [Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$check$1.apply(TimeoutSolver.scala:32) [Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$check$1.apply(TimeoutSolver.scala:32) [Internal] - inox.utils.TimeoutFor.interruptAfter(TimeoutFor.scala:36) [Internal] - inox.solvers.combinators.TimeoutSolver$class.check(TimeoutSolver.scala:31) [Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$tip$TipDebugger$$super$check(SolverFactory.scala:122) [Internal] - inox.tip.TipDebugger$class.check(TipDebugger.scala:56) [Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.check(SolverFactory.scala:122) [Internal] - inox.solvers.SimpleSolverAPI$class.solveVALID(SimpleSolverAPI.scala:22) [Internal] - inox.solvers.SimpleSolverAPI$$anon$1.solveVALID(SimpleSolverAPI.scala:57) [Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7$$anonfun$8.apply(RelationProcessor.scala:46) [Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7$$anonfun$8.apply(RelationProcessor.scala:45) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.immutable.Set$Set2.foreach(Set.scala:128) [Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234) [Internal] - scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47) [Internal] - scala.collection.SetLike$class.map(SetLike.scala:92) [Internal] - scala.collection.AbstractSet.map(Set.scala:47) [Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7.apply(RelationProcessor.scala:45) [Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7.apply(RelationProcessor.scala:44) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) [Internal] - scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59) [Internal] - scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48) [Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234) [Internal] - scala.collection.AbstractTraversable.map(Traversable.scala:104) [Internal] - stainless.termination.RelationProcessor$$anonfun$run$1.apply(RelationProcessor.scala:44) [Internal] - stainless.termination.RelationProcessor$$anonfun$run$1.apply(RelationProcessor.scala:21) [Internal] - scala.util.Try$.apply(Try.scala:192) [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93) [Internal] - inox.utils.TimerStorage.run(Timer.scala:88) [Internal] - stainless.termination.RelationProcessor$class.run(RelationProcessor.scala:21) [Internal] - stainless.termination.TerminationChecker$$anon$1$lexicographicProcessor$.run(TerminationChecker.scala:110) [Internal] - stainless.termination.ProcessingPipeline$$anon$1.next(ProcessingPipeline.scala:204) [Internal] - stainless.termination.ProcessingPipeline$$anon$1.next(ProcessingPipeline.scala:197) [Internal] - scala.collection.Iterator$$anon$13.hasNext(Iterator.scala:462) [Internal] - scala.collection.Iterator$class.foreach(Iterator.scala:893) [Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1336) [Internal] - stainless.termination.ProcessingPipeline$class.runPipeline(ProcessingPipeline.scala:232) [Internal] - stainless.termination.ProcessingPipeline$class.terminates(ProcessingPipeline.scala:156) [Internal] - stainless.termination.TerminationChecker$$anon$1.terminates(TerminationChecker.scala:39) [Internal] - stainless.termination.TerminationComponent$$anonfun$2$$anonfun$3.apply(TerminationComponent.scala:60) [Internal] - stainless.termination.TerminationComponent$$anonfun$2$$anonfun$3.apply(TerminationComponent.scala:60) [Internal] - scala.util.Try$.apply(Try.scala:192) [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93) [Internal] - stainless.termination.TerminationComponent$$anonfun$2.apply(TerminationComponent.scala:60) [Internal] - stainless.termination.TerminationComponent$$anonfun$2.apply(TerminationComponent.scala:59) [Internal] - scala.collection.immutable.Stream$$anonfun$map$1.apply(Stream.scala:418) [Internal] - scala.collection.immutable.Stream$$anonfun$map$1.apply(Stream.scala:418) [Internal] - scala.collection.immutable.Stream$Cons.tail(Stream.scala:1233) [Internal] - scala.collection.immutable.Stream$Cons.tail(Stream.scala:1223) [Internal] - scala.collection.immutable.Stream.foreach(Stream.scala:595) [Internal] - scala.collection.TraversableOnce$class.toMap(TraversableOnce.scala:316) [Internal] - scala.collection.AbstractTraversable.toMap(Traversable.scala:104) [Internal] - stainless.termination.TerminationComponent$$anon$2.(TerminationComponent.scala:69) [Internal] - stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:67) [Internal] - stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:8) [Internal] - stainless.SimpleComponent$class.apply(Component.scala:87) [Internal] - stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:8) [Internal] - stainless.termination.TerminationCallBack.solve(TerminationCallBack.scala:28) [Internal] - stainless.termination.TerminationCallBack.solve(TerminationCallBack.scala:12) [Internal] - stainless.frontend.CallBackWithRegistry$$anon$2.call(CallBackWithRegistry.scala:191) [Internal] - stainless.frontend.CallBackWithRegistry$$anon$2.call(CallBackWithRegistry.scala:190) [Internal] - java.util.concurrent.FutureTask.run(FutureTask.java:266) [Internal] - java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149) [Internal] - java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624) [Internal] - java.lang.Thread.run(Thread.java:748) ```

epfl-lara / inox

"String index out of range: 0" in ASCIIStringEncoder #58