Created
March 1, 2018 12:01
-
-
Save jad-hamza/5a501b40afce3fa9fc086c2f155d22e0 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [Internal] Error: assertion failed. Trace: | |
| [Internal] - scala.Predef$.assert(Predef.scala:156) | |
| [Internal] - inox.ast.Paths$Path.withBound(Paths.scala:96) | |
| [Internal] - inox.ast.Paths$Path.withBound(Paths.scala:76) | |
| [Internal] - inox.ast.Paths$PathLike$$anonfun$withBounds$1.apply(Paths.scala:20) | |
| [Internal] - inox.ast.Paths$PathLike$$anonfun$withBounds$1.apply(Paths.scala:20) | |
| [Internal] - scala.collection.LinearSeqOptimized$class.foldLeft(LinearSeqOptimized.scala:124) | |
| [Internal] - scala.collection.immutable.List.foldLeft(List.scala:84) | |
| [Internal] - inox.ast.Paths$PathLike$class.withBounds(Paths.scala:20) | |
| [Internal] - inox.ast.Paths$Path.withBounds(Paths.scala:76) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:25) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$$anonfun$rec$1.apply(TransformerWithPC.scala:44) | |
| [Internal] - inox.transformers.TransformerWithPC$$anonfun$rec$1.apply(TransformerWithPC.scala:43) | |
| [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] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:43) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$$anonfun$rec$2.apply(TransformerWithPC.scala:52) | |
| [Internal] - inox.transformers.TransformerWithPC$$anonfun$rec$2.apply(TransformerWithPC.scala:51) | |
| [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] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:51) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:38) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:16) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:17) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:39) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:17) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.Transformer$class.transform(Transformer.scala:28) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithPC.transform(SymbolOps.scala:1147) | |
| [Internal] - inox.transformers.Transformer$class.transform(Transformer.scala:30) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithPC.transform(SymbolOps.scala:1147) | |
| [Internal] - inox.ast.SymbolOps$class.transformWithPC(SymbolOps.scala:1165) | |
| [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.transformWithPC(SimpleSymbols.scala:12) | |
| [Internal] - inox.ast.SymbolOps$class.existsWithPC(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.existsWithPC(SimpleSymbols.scala:12) | |
| [Internal] - inox.ast.SymbolOps$class.existsWithPC(SymbolOps.scala:1200) | |
| [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.existsWithPC(SimpleSymbols.scala:12) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.immediateCall$lzycompute$1(SimplifierWithPC.scala:350) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.immediateCall$1(SimplifierWithPC.scala:350) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.apply(SimplifierWithPC.scala:362) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.apply(SimplifierWithPC.scala:343) | |
| [Internal] - scala.Option.getOrElse(Option.scala:121) | |
| [Internal] - inox.transformers.SimplifierWithPC$class.inox$transformers$SimplifierWithPC$$simplify(SimplifierWithPC.scala:343) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.apply(SimplifierWithPC.scala:344) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.apply(SimplifierWithPC.scala:343) | |
| [Internal] - scala.Option.getOrElse(Option.scala:121) | |
| [Internal] - inox.transformers.SimplifierWithPC$class.inox$transformers$SimplifierWithPC$$simplify(SimplifierWithPC.scala:343) | |
| [Internal] - inox.transformers.SimplifierWithPC$class.rec(SimplifierWithPC.scala:436) | |
| [Internal] - inox.ast.SymbolOps$SimplifierWithPC.rec(SymbolOps.scala:31) | |
| [Internal] - inox.ast.SymbolOps$SimplifierWithPC.rec(SymbolOps.scala:31) | |
| [Internal] - inox.transformers.Transformer$class.transform(Transformer.scala:28) | |
| [Internal] - inox.ast.SymbolOps$SimplifierWithPC.transform(SymbolOps.scala:31) | |
| [Internal] - inox.transformers.Transformer$class.transform(Transformer.scala:30) | |
| [Internal] - inox.ast.SymbolOps$SimplifierWithPC.transform(SymbolOps.scala:31) | |
| [Internal] - inox.ast.SymbolOps$class.simplifyExpr(SymbolOps.scala:73) | |
| [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.simplifyExpr(SimpleSymbols.scala:12) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$61.apply(SymbolOps.scala:1124) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$61.apply(SymbolOps.scala:1124) | |
| [Internal] - scala.Function1$$anonfun$compose$1.apply(Function1.scala:44) | |
| [Internal] - scala.Function1$$anonfun$compose$1.apply(Function1.scala:44) | |
| [Internal] - scala.Function1$$anonfun$compose$1.apply(Function1.scala:44) | |
| [Internal] - scala.Function1$$anonfun$compose$1.apply(Function1.scala:44) | |
| [Internal] - inox.ast.SymbolOps$class.simplifyFormula(SymbolOps.scala:1128) | |
| [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.simplifyFormula(SimpleSymbols.scala:12) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$$anonfun$apply$1$$anonfun$1.apply(FunctionTemplates.scala:23) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$$anonfun$apply$1$$anonfun$1.apply(FunctionTemplates.scala:23) | |
| [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.FunctionTemplates$FunctionTemplate$$anonfun$apply$1.apply(FunctionTemplates.scala:23) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$$anonfun$apply$1.apply(FunctionTemplates.scala:22) | |
| [Internal] - scala.collection.mutable.MapLike$class.getOrElseUpdate(MapLike.scala:194) | |
| [Internal] - scala.collection.mutable.AbstractMap.getOrElseUpdate(Map.scala:80) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$.apply(FunctionTemplates.scala:22) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$$anonfun$unroll$4$$anonfun$apply$6.apply(FunctionTemplates.scala:164) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$$anonfun$unroll$4$$anonfun$apply$6.apply(FunctionTemplates.scala:131) | |
| [Internal] - scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733) | |
| [Internal] - scala.collection.immutable.Set$Set1.foreach(Set.scala:94) | |
| [Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$$anonfun$unroll$4.apply(FunctionTemplates.scala:131) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$$anonfun$unroll$4.apply(FunctionTemplates.scala:129) | |
| [Internal] - scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59) | |
| [Internal] - scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.unroll(FunctionTemplates.scala:129) | |
| [Internal] - inox.solvers.unrolling.Templates$$anonfun$unroll$4.apply(Templates.scala:79) | |
| [Internal] - inox.solvers.unrolling.Templates$$anonfun$unroll$4.apply(Templates.scala:79) | |
| [Internal] - scala.collection.TraversableLike$$anonfun$flatMap$1.apply(TraversableLike.scala:241) | |
| [Internal] - scala.collection.TraversableLike$$anonfun$flatMap$1.apply(TraversableLike.scala:241) | |
| [Internal] - scala.collection.immutable.List.foreach(List.scala:381) | |
| [Internal] - scala.collection.TraversableLike$class.flatMap(TraversableLike.scala:241) | |
| [Internal] - scala.collection.immutable.List.flatMap(List.scala:344) | |
| [Internal] - inox.solvers.unrolling.Templates$class.unroll(Templates.scala:79) | |
| [Internal] - inox.solvers.z3.Z3Unrolling$templates$.unroll(Z3Unrolling.scala:28) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1$$anonfun$apply$44$$anonfun$apply$2.apply$mcVI$sp(UnrollingSolver.scala:701) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1$$anonfun$apply$44$$anonfun$apply$2.apply(UnrollingSolver.scala:700) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1$$anonfun$apply$44$$anonfun$apply$2.apply(UnrollingSolver.scala:700) | |
| [Internal] - scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733) | |
| [Internal] - scala.collection.immutable.Range.foreach(Range.scala:160) | |
| [Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1$$anonfun$apply$44.apply(UnrollingSolver.scala:700) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1$$anonfun$apply$44.apply(UnrollingSolver.scala:696) | |
| [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$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:696) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:464) | |
| [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:464) | |
| [Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:122) | |
| [Internal] - inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:47) | |
| [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$class.check(TimeoutSolver.scala:35) | |
| [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] - stainless.verification.VerificationChecker$$anonfun$3.apply(VerificationChecker.scala:104) | |
| [Internal] - stainless.verification.VerificationChecker$$anonfun$3.apply(VerificationChecker.scala:102) | |
| [Internal] - scala.util.Try$.apply(Try.scala:192) | |
| [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93) | |
| [Internal] - stainless.verification.VerificationChecker$class.checkVC(VerificationChecker.scala:102) | |
| [Internal] - stainless.verification.VerificationChecker$$anon$1.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:170) | |
| [Internal] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:70) | |
| [Internal] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:50) | |
| [Internal] - scala.util.Try$.apply(Try.scala:192) | |
| [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93) | |
| [Internal] - stainless.verification.VerificationCache$class.checkVC(VerificationCache.scala:50) | |
| [Internal] - stainless.verification.VerificationChecker$$anon$1.checkVC(VerificationChecker.scala:170) | |
| [Internal] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:72) | |
| [Internal] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:70) | |
| [Internal] - scala.collection.parallel.AugmentedIterableIterator$class.flatmap2combiner(RemainsIterator.scala:132) | |
| [Internal] - scala.collection.parallel.immutable.ParVector$ParVectorIterator.flatmap2combiner(ParVector.scala:62) | |
| [Internal] - scala.collection.parallel.ParIterableLike$FlatMap.leaf(ParIterableLike.scala:1072) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply$mcV$sp(Tasks.scala:49) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48) | |
| [Internal] - scala.collection.parallel.Task$class.tryLeaf(Tasks.scala:51) | |
| [Internal] - scala.collection.parallel.ParIterableLike$FlatMap.tryLeaf(ParIterableLike.scala:1068) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask$class.internal(Tasks.scala:159) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.internal(Tasks.scala:443) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask$class.compute(Tasks.scala:149) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.compute(Tasks.scala:443) | |
| [Internal] - scala.concurrent.forkjoin.RecursiveAction.exec(RecursiveAction.java:160) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1339) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107) | |
| [Internal] assertion failed | |
| [Internal] Please inform the authors of Inox about this message | |
| [Internal] Error: assertion failed. Trace: | |
| [Internal] - scala.Predef$.assert(Predef.scala:156) | |
| [Internal] - inox.ast.Paths$Path.withBound(Paths.scala:96) | |
| [Internal] - inox.ast.Paths$Path.withBound(Paths.scala:76) | |
| [Internal] - inox.ast.Paths$PathLike$$anonfun$withBounds$1.apply(Paths.scala:20) | |
| [Internal] - inox.ast.Paths$PathLike$$anonfun$withBounds$1.apply(Paths.scala:20) | |
| [Internal] - scala.collection.LinearSeqOptimized$class.foldLeft(LinearSeqOptimized.scala:124) | |
| [Internal] - scala.collection.immutable.List.foldLeft(List.scala:84) | |
| [Internal] - inox.ast.Paths$PathLike$class.withBounds(Paths.scala:20) | |
| [Internal] - inox.ast.Paths$Path.withBounds(Paths.scala:76) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:25) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$$anonfun$rec$1.apply(TransformerWithPC.scala:44) | |
| [Internal] - inox.transformers.TransformerWithPC$$anonfun$rec$1.apply(TransformerWithPC.scala:43) | |
| [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] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:43) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$$anonfun$rec$2.apply(TransformerWithPC.scala:52) | |
| [Internal] - inox.transformers.TransformerWithPC$$anonfun$rec$2.apply(TransformerWithPC.scala:51) | |
| [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] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:51) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:38) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:16) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:17) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:39) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.TransformerWithPC$class.rec(TransformerWithPC.scala:17) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.inox$ast$SymbolOps$TransformerWithFun$$super$rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$$anonfun$66.apply(SymbolOps.scala:1142) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1194) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$existsWithPC$1.apply(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithFun$class.rec(SymbolOps.scala:1144) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.ast.SymbolOps$$anon$1.rec(SymbolOps.scala:1159) | |
| [Internal] - inox.transformers.Transformer$class.transform(Transformer.scala:28) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithPC.transform(SymbolOps.scala:1147) | |
| [Internal] - inox.transformers.Transformer$class.transform(Transformer.scala:30) | |
| [Internal] - inox.ast.SymbolOps$TransformerWithPC.transform(SymbolOps.scala:1147) | |
| [Internal] - inox.ast.SymbolOps$class.transformWithPC(SymbolOps.scala:1165) | |
| [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.transformWithPC(SimpleSymbols.scala:12) | |
| [Internal] - inox.ast.SymbolOps$class.existsWithPC(SymbolOps.scala:1189) | |
| [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.existsWithPC(SimpleSymbols.scala:12) | |
| [Internal] - inox.ast.SymbolOps$class.existsWithPC(SymbolOps.scala:1200) | |
| [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.existsWithPC(SimpleSymbols.scala:12) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.immediateCall$lzycompute$1(SimplifierWithPC.scala:350) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.immediateCall$1(SimplifierWithPC.scala:350) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.apply(SimplifierWithPC.scala:362) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.apply(SimplifierWithPC.scala:343) | |
| [Internal] - scala.Option.getOrElse(Option.scala:121) | |
| [Internal] - inox.transformers.SimplifierWithPC$class.inox$transformers$SimplifierWithPC$$simplify(SimplifierWithPC.scala:343) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.apply(SimplifierWithPC.scala:344) | |
| [Internal] - inox.transformers.SimplifierWithPC$$anonfun$inox$transformers$SimplifierWithPC$$simplify$5.apply(SimplifierWithPC.scala:343) | |
| [Internal] - scala.Option.getOrElse(Option.scala:121) | |
| [Internal] - inox.transformers.SimplifierWithPC$class.inox$transformers$SimplifierWithPC$$simplify(SimplifierWithPC.scala:343) | |
| [Internal] - inox.transformers.SimplifierWithPC$class.rec(SimplifierWithPC.scala:436) | |
| [Internal] - inox.ast.SymbolOps$SimplifierWithPC.rec(SymbolOps.scala:31) | |
| [Internal] - inox.ast.SymbolOps$SimplifierWithPC.rec(SymbolOps.scala:31) | |
| [Internal] - inox.transformers.Transformer$class.transform(Transformer.scala:28) | |
| [Internal] - inox.ast.SymbolOps$SimplifierWithPC.transform(SymbolOps.scala:31) | |
| [Internal] - inox.transformers.Transformer$class.transform(Transformer.scala:30) | |
| [Internal] - inox.ast.SymbolOps$SimplifierWithPC.transform(SymbolOps.scala:31) | |
| [Internal] - inox.ast.SymbolOps$class.simplifyExpr(SymbolOps.scala:73) | |
| [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.simplifyExpr(SimpleSymbols.scala:12) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$61.apply(SymbolOps.scala:1124) | |
| [Internal] - inox.ast.SymbolOps$$anonfun$61.apply(SymbolOps.scala:1124) | |
| [Internal] - scala.Function1$$anonfun$compose$1.apply(Function1.scala:44) | |
| [Internal] - scala.Function1$$anonfun$compose$1.apply(Function1.scala:44) | |
| [Internal] - scala.Function1$$anonfun$compose$1.apply(Function1.scala:44) | |
| [Internal] - scala.Function1$$anonfun$compose$1.apply(Function1.scala:44) | |
| [Internal] - inox.ast.SymbolOps$class.simplifyFormula(SymbolOps.scala:1128) | |
| [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.simplifyFormula(SimpleSymbols.scala:12) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$$anonfun$apply$1$$anonfun$1.apply(FunctionTemplates.scala:23) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$$anonfun$apply$1$$anonfun$1.apply(FunctionTemplates.scala:23) | |
| [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.FunctionTemplates$FunctionTemplate$$anonfun$apply$1.apply(FunctionTemplates.scala:23) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$$anonfun$apply$1.apply(FunctionTemplates.scala:22) | |
| [Internal] - scala.collection.mutable.MapLike$class.getOrElseUpdate(MapLike.scala:194) | |
| [Internal] - scala.collection.mutable.AbstractMap.getOrElseUpdate(Map.scala:80) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$.apply(FunctionTemplates.scala:22) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$$anonfun$unroll$4$$anonfun$apply$6.apply(FunctionTemplates.scala:164) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$$anonfun$unroll$4$$anonfun$apply$6.apply(FunctionTemplates.scala:131) | |
| [Internal] - scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733) | |
| [Internal] - scala.collection.immutable.Set$Set1.foreach(Set.scala:94) | |
| [Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$$anonfun$unroll$4.apply(FunctionTemplates.scala:131) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$$anonfun$unroll$4.apply(FunctionTemplates.scala:129) | |
| [Internal] - scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59) | |
| [Internal] - scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48) | |
| [Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.unroll(FunctionTemplates.scala:129) | |
| [Internal] - inox.solvers.unrolling.Templates$$anonfun$unroll$4.apply(Templates.scala:79) | |
| [Internal] - inox.solvers.unrolling.Templates$$anonfun$unroll$4.apply(Templates.scala:79) | |
| [Internal] - scala.collection.TraversableLike$$anonfun$flatMap$1.apply(TraversableLike.scala:241) | |
| [Internal] - scala.collection.TraversableLike$$anonfun$flatMap$1.apply(TraversableLike.scala:241) | |
| [Internal] - scala.collection.immutable.List.foreach(List.scala:381) | |
| [Internal] - scala.collection.TraversableLike$class.flatMap(TraversableLike.scala:241) | |
| [Internal] - scala.collection.immutable.List.flatMap(List.scala:344) | |
| [Internal] - inox.solvers.unrolling.Templates$class.unroll(Templates.scala:79) | |
| [Internal] - inox.solvers.z3.Z3Unrolling$templates$.unroll(Z3Unrolling.scala:28) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1$$anonfun$apply$44$$anonfun$apply$2.apply$mcVI$sp(UnrollingSolver.scala:701) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1$$anonfun$apply$44$$anonfun$apply$2.apply(UnrollingSolver.scala:700) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1$$anonfun$apply$44$$anonfun$apply$2.apply(UnrollingSolver.scala:700) | |
| [Internal] - scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733) | |
| [Internal] - scala.collection.immutable.Range.foreach(Range.scala:160) | |
| [Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1$$anonfun$apply$44.apply(UnrollingSolver.scala:700) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1$$anonfun$apply$44.apply(UnrollingSolver.scala:696) | |
| [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$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:696) | |
| [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:464) | |
| [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:464) | |
| [Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:122) | |
| [Internal] - inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:47) | |
| [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$class.check(TimeoutSolver.scala:35) | |
| [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] - stainless.verification.VerificationChecker$$anonfun$3.apply(VerificationChecker.scala:104) | |
| [Internal] - stainless.verification.VerificationChecker$$anonfun$3.apply(VerificationChecker.scala:102) | |
| [Internal] - scala.util.Try$.apply(Try.scala:192) | |
| [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93) | |
| [Internal] - stainless.verification.VerificationChecker$class.checkVC(VerificationChecker.scala:102) | |
| [Internal] - stainless.verification.VerificationChecker$$anon$1.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:170) | |
| [Internal] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:70) | |
| [Internal] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:50) | |
| [Internal] - scala.util.Try$.apply(Try.scala:192) | |
| [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93) | |
| [Internal] - stainless.verification.VerificationCache$class.checkVC(VerificationCache.scala:50) | |
| [Internal] - stainless.verification.VerificationChecker$$anon$1.checkVC(VerificationChecker.scala:170) | |
| [Internal] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:72) | |
| [Internal] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:70) | |
| [Internal] - scala.collection.parallel.AugmentedIterableIterator$class.flatmap2combiner(RemainsIterator.scala:132) | |
| [Internal] - scala.collection.parallel.immutable.ParVector$ParVectorIterator.flatmap2combiner(ParVector.scala:62) | |
| [Internal] - scala.collection.parallel.ParIterableLike$FlatMap.leaf(ParIterableLike.scala:1072) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply$mcV$sp(Tasks.scala:49) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48) | |
| [Internal] - scala.collection.parallel.Task$class.tryLeaf(Tasks.scala:51) | |
| [Internal] - scala.collection.parallel.ParIterableLike$FlatMap.tryLeaf(ParIterableLike.scala:1068) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask$class.compute(Tasks.scala:152) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.compute(Tasks.scala:443) | |
| [Internal] - scala.concurrent.forkjoin.RecursiveAction.exec(RecursiveAction.java:160) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1339) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107) | |
| [Internal] Error: assertion failed. Trace: | |
| [Internal] - inox.Reporter.onFatal(Reporter.scala:39) | |
| [Internal] - inox.Reporter.internalError(Reporter.scala:57) | |
| [Internal] - inox.Reporter.internalError(Reporter.scala:100) | |
| [Internal] - inox.Reporter.internalError(Reporter.scala:103) | |
| [Internal] - stainless.verification.VerificationChecker$class.checkVC(VerificationChecker.scala:132) | |
| [Internal] - stainless.verification.VerificationChecker$$anon$1.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:170) | |
| [Internal] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:70) | |
| [Internal] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:50) | |
| [Internal] - scala.util.Try$.apply(Try.scala:192) | |
| [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93) | |
| [Internal] - stainless.verification.VerificationCache$class.checkVC(VerificationCache.scala:50) | |
| [Internal] - stainless.verification.VerificationChecker$$anon$1.checkVC(VerificationChecker.scala:170) | |
| [Internal] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:72) | |
| [Internal] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:70) | |
| [Internal] - scala.collection.parallel.AugmentedIterableIterator$class.flatmap2combiner(RemainsIterator.scala:132) | |
| [Internal] - scala.collection.parallel.immutable.ParVector$ParVectorIterator.flatmap2combiner(ParVector.scala:62) | |
| [Internal] - scala.collection.parallel.ParIterableLike$FlatMap.leaf(ParIterableLike.scala:1072) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply$mcV$sp(Tasks.scala:49) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48) | |
| [Internal] - scala.collection.parallel.Task$class.tryLeaf(Tasks.scala:51) | |
| [Internal] - scala.collection.parallel.ParIterableLike$FlatMap.tryLeaf(ParIterableLike.scala:1068) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask$class.internal(Tasks.scala:159) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.internal(Tasks.scala:443) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask$class.compute(Tasks.scala:149) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.compute(Tasks.scala:443) | |
| [Internal] - scala.concurrent.forkjoin.RecursiveAction.exec(RecursiveAction.java:160) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1339) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107) | |
| [Internal] assertion failed | |
| [Internal] Please inform the authors of Inox about this message | |
| [Internal] assertion failed | |
| [Internal] Please inform the authors of Inox about this message | |
| [Internal] Error: assertion failed. Trace: | |
| [Internal] - inox.Reporter.onFatal(Reporter.scala:39) | |
| [Internal] - inox.Reporter.internalError(Reporter.scala:57) | |
| [Internal] - inox.Reporter.internalError(Reporter.scala:100) | |
| [Internal] - inox.Reporter.internalError(Reporter.scala:103) | |
| [Internal] - stainless.verification.VerificationChecker$class.checkVC(VerificationChecker.scala:132) | |
| [Internal] - stainless.verification.VerificationChecker$$anon$1.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:170) | |
| [Internal] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:70) | |
| [Internal] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:50) | |
| [Internal] - scala.util.Try$.apply(Try.scala:192) | |
| [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93) | |
| [Internal] - stainless.verification.VerificationCache$class.checkVC(VerificationCache.scala:50) | |
| [Internal] - stainless.verification.VerificationChecker$$anon$1.checkVC(VerificationChecker.scala:170) | |
| [Internal] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:72) | |
| [Internal] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:70) | |
| [Internal] - scala.collection.parallel.AugmentedIterableIterator$class.flatmap2combiner(RemainsIterator.scala:132) | |
| [Internal] - scala.collection.parallel.immutable.ParVector$ParVectorIterator.flatmap2combiner(ParVector.scala:62) | |
| [Internal] - scala.collection.parallel.ParIterableLike$FlatMap.leaf(ParIterableLike.scala:1072) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply$mcV$sp(Tasks.scala:49) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48) | |
| [Internal] - scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48) | |
| [Internal] - scala.collection.parallel.Task$class.tryLeaf(Tasks.scala:51) | |
| [Internal] - scala.collection.parallel.ParIterableLike$FlatMap.tryLeaf(ParIterableLike.scala:1068) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask$class.compute(Tasks.scala:152) | |
| [Internal] - scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.compute(Tasks.scala:443) | |
| [Internal] - scala.concurrent.forkjoin.RecursiveAction.exec(RecursiveAction.java:160) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1339) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979) | |
| [Internal] - scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107) | |
| [Internal] assertion failed | |
| [Internal] Please inform the authors of Inox about this message |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment