Fix chor/endpointexpr checking errors in TTTlast. Unfortunately, now … #2698
GitHub Actions / TestReport
failed
Sep 20, 2024 in 1s
1053 passed, 6 failed and 44 skipped
Report exceeded GitHub limit of 65535 bytes and has been trimmed
Annotations
Check failure on line 190 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec ► TTTlast case study (choreography verification) verifies with silicon
Failed test found in:
reports/ubuntu-0/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml
Error:
org.scalatest.exceptions.TestFailedDueToTimeoutException: The code passed to failAfter did not complete within 300 seconds.Raw output
org.scalatest.exceptions.TestFailedDueToTimeoutException: The code passed to failAfter did not complete within 300 seconds.
at java.base/java.lang.Thread.getStackTrace(Thread.java:1619)
at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:277)
at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3(VeyMontSpec.scala:190)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3$adapted(VeyMontSpec.scala:176)
at hre.util.FilesHelper$.withTempDir(FilesHelper.scala:11)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$2(VeyMontSpec.scala:176)
at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
at org.scalatest.Transformer.apply(Transformer.scala:22)
at org.scalatest.Transformer.apply(Transformer.scala:20)
at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
at scala.collection.immutable.List.foreach(List.scala:333)
at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
at org.scalatest.Suite.run(Suite.scala:1112)
at org.scalatest.Suite.run$(Suite.scala:1094)
at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
at org.scalatest.Suite.run(Suite.scala:1109)
at org.scalatest.Suite.run$(Suite.scala:1094)
at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
at scala.collection.immutable.List.foreach(List.scala:333)
at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
at org.scalatest.tools.Runner$.main(Runner.scala:775)
at org.scalatest.tools.Runner.main(Runner.scala)
Cause: java.lang.StackOverflowError
at viper.silicon.decider.TermToSMTLib2Converter.render(TermToSMTLib2Converter.scala:210)
at viper.silicon.decider.TermToSMTLib2Converter.renderBinaryOp(TermToSMTLib2Converter.scala:336)
at viper.silicon.decider.TermToSMTLib2Converter.render(TermToSMTLib2Converter.scala:175)
at viper.silicon.decider.TermToSMTLib2Converter.$anonfun$renderNAryOp$1(TermToSMTLib2Converter.scala:344)
at scala.collection.immutable.ArraySeq.map(ArraySeq.scala:75)
at scala.collection.immutable.ArraySeq.map(ArraySeq.scala:35)
at viper.silicon.decider.TermToSMTLib2Converter.renderNAryOp(TermToSMTLib2Converter.scala:344)
at viper.silicon.decider.TermToSMTLib2Converter.render(TermToSMTLib2Converter.scala:167)
at viper.silicon.decider.TermToSMTLib2Converter.convert(TermToSMTLib2Converter.scala:103)
at viper.silicon.decider.ProverStdIO.assert(ProverStdIO.scala:235)
at viper.silicon.decider.DefaultDeciderProvider$decider$.proverAssert(Decider.scala:326)
at viper.silicon.decider.DefaultDeciderProvider$decider$.deciderAssert(Decider.scala:308)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:289)
at viper.silicon.rules.permissionSupporter$.assertNotNegative(PermissionSupporter.scala:26)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$33(Consumer.scala:416)
at viper.silicon.rules.evaluator$.$anonfun$evalLocationAccess$3(Evaluator.scala:1254)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:163)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:163)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.evals(Evaluator.scala:72)
at viper.silicon.rules.evaluator$.evalLocationAccess(Evaluator.scala:1253)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$32(Consumer.scala:415)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1297)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1297)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1(Evaluator.scala:1312)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1$adapted(Evaluator.scala:1311)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:300)
at viper.silicon.rules.evaluator$.failIfDivByZero(Evaluator.scala:1311)
at viper.silicon.rules.evaluator$.$anonfun$eval2$31(Evaluator.scala:443)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$30(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:441)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1296)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1283)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:433)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1296)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1283)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:433)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.consumer$.consumeTlc(Consumer.scala:414)
at viper.silicon.rules.consumer$.$anonfun$wrappedConsumeTlc$1(Consumer.scala:164)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$1(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.tryOrFailWithResult(ExecutionFlowController.scala:118)
at viper.silicon.rules.executionFlowController$.tryOrFail2(ExecutionFlowController.scala:174)
at viper.silicon.rules.consumer$.wrappedConsumeTlc(Consumer.scala:167)
at viper.silicon.rules.consumer$.consumeTlcs(Consumer.scala:123)
at viper.silicon.rules.consumer$.$anonfun$consumeTlcs$1(Consumer.scala:126)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$3(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFailWithResult$1(ExecutionFlowController.scala:120)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$2(ExecutionFlowController.scala:174)
at viper.silicon.rules.consumer$.$anonfun$wrappedConsumeTlc$2(Consumer.scala:166)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$35(Consumer.scala:427)
at viper.silicon.rules.chunkSupporter$.$anonfun$consume$1(ChunkSupporter.scala:79)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$3(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFailWithResult$1(ExecutionFlowController.scala:120)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$2(ExecutionFlowController.scala:174)
at viper.silicon.rules.chunkSupporter$.$anonfun$consume2$4(ChunkSupporter.scala:127)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$1(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.tryOrFailWithResult(ExecutionFlowController.scala:118)
at viper.silicon.rules.executionFlowController$.tryOrFail2(ExecutionFlowController.scala:174)
at viper.silicon.rules.chunkSupporter$.consume2(ChunkSupporter.scala:134)
at viper.silicon.rules.chunkSupporter$.consume(ChunkSupporter.scala:76)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$34(Consumer.scala:424)
at viper.silicon.rules.permissionSupporter$.$anonfun$assertNotNegative$1(PermissionSupporter.scala:27)
at viper.silicon.rules.permissionSupporter$.$anonfun$assertNotNegative$1$adapted(PermissionSupporter.scala:26)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:300)
at viper.silicon.rules.permissionSupporter$.assertNotNegative(PermissionSupporter.scala:26)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$33(Consumer.scala:416)
at viper.silicon.rules.evaluator$.$anonfun$evalLocationAccess$1(Evaluator.scala:1251)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:163)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalLocationAccess(Evaluator.scala:1250)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$32(Consumer.scala:415)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1297)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1297)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1(Evaluator.scala:1312)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1$adapted(Evaluator.scala:1311)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:300)
at viper.silicon.rules.evaluator$.failIfDivByZero(Evaluator.scala:1311)
at viper.silicon.rules.evaluator$.$anonfun$eval2$31(Evaluator.scala:443)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$30(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:441)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1296)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1283)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:433)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1296)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1283)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:433)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.consumer$.consumeTlc(Consumer.scala:414)
at viper.silicon.rules.consumer$.$anonfun$wrappedConsumeTlc$1(Consumer.scala:164)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$1(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.tryOrFailWithResult(ExecutionFlowController.scala:118)
at viper.silicon.rules.executionFlowController$.tryOrFail2(ExecutionFlowController.scala:174)
at viper.silicon.rules.consumer$.wrappedConsumeTlc(Consumer.scala:167)
at viper.silicon.rules.consumer$.consumeTlcs(Consumer.scala:125)
at viper.silicon.rules.consumer$.$anonfun$consumeTlcs$1(Consumer.scala:126)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$3(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFailWithResult$1(ExecutionFlowController.scala:120)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$2(ExecutionFlowController.scala:174)
at viper.silicon.rules.consumer$.$anonfun$wrappedConsumeTlc$2(Consumer.scala:166)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$35(Consumer.scala:427)
at viper.silicon.rules.chunkSupporter$.$anonfun$consume$1(ChunkSupporter.scala:79)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$3(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFailWithResult$1(ExecutionFlowController.scala:120)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$2(ExecutionFlowController.scala:174)
at viper.silicon.rules.chunkSupporter$.$anonfun$consume2$4(ChunkSupporter.scala:127)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$1(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.tryOrFailWithResult(ExecutionFlowController.scala:118)
at viper.silicon.rules.executionFlowController$.tryOrFail2(ExecutionFlowController.scala:174)
at viper.silicon.rules.chunkSupporter$.consume2(ChunkSupporter.scala:134)
at viper.silicon.rules.chunkSupporter$.consume(ChunkSupporter.scala:76)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$34(Consumer.scala:424)
at viper.silicon.rules.permissionSupporter$.$anonfun$assertNotNegative$1(PermissionSupporter.scala:27)
at viper.silicon.rules.permissionSupporter$.$anonfun$assertNotNegative$1$adapted(PermissionSupporter.scala:26)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:300)
at viper.silicon.rules.permissionSupporter$.assertNotNegative(PermissionSupporter.scala:26)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$33(Consumer.scala:416)
at viper.silicon.rules.evaluator$.$anonfun$evalLocationAccess$3(Evaluator.scala:1254)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:163)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:163)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.evals(Evaluator.scala:72)
at viper.silicon.rules.evaluator$.evalLocationAccess(Evaluator.scala:1253)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$32(Consumer.scala:415)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1297)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1297)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1(Evaluator.scala:1312)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1$adapted(Evaluator.scala:1311)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:300)
at viper.silicon.rules.evaluator$.failIfDivByZero(Evaluator.scala:1311)
at viper.silicon.rules.evaluator$.$anonfun$eval2$31(Evaluator.scala:443)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$30(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:441)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1296)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1283)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:433)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1296)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1283)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:433)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.consumer$.consumeTlc(Consumer.scala:414)
at viper.silicon.rules.consumer$.$anonfun$wrappedConsumeTlc$1(Consumer.scala:164)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$1(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.tryOrFailWithResult(ExecutionFlowController.scala:118)
at viper.silicon.rules.executionFlowController$.tryOrFail2(ExecutionFlowController.scala:174)
at viper.silicon.rules.consumer$.wrappedConsumeTlc(Consumer.scala:167)
at viper.silicon.rules.consumer$.consumeTlcs(Consumer.scala:125)
at viper.silicon.rules.consumer$.$anonfun$consumeTlcs$1(Consumer.scala:126)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$3(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFailWithResult$1(ExecutionFlowController.scala:120)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$2(ExecutionFlowController.scala:174)
at viper.silicon.rules.consumer$.$anonfun$wrappedConsumeTlc$2(Consumer.scala:166)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$35(Consumer.scala:427)
at viper.silicon.rules.chunkSupporter$.$anonfun$consume$1(ChunkSupporter.scala:79)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$3(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFailWithResult$1(ExecutionFlowController.scala:120)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$2(ExecutionFlowController.scala:174)
at viper.silicon.rules.chunkSupporter$.$anonfun$consume2$4(ChunkSupporter.scala:127)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$1(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.tryOrFailWithResult(ExecutionFlowController.scala:118)
at viper.silicon.rules.executionFlowController$.tryOrFail2(ExecutionFlowController.scala:174)
at viper.silicon.rules.chunkSupporter$.consume2(ChunkSupporter.scala:134)
at viper.silicon.rules.chunkSupporter$.consume(ChunkSupporter.scala:76)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$34(Consumer.scala:424)
at viper.silicon.rules.permissionSupporter$.$anonfun$assertNotNegative$1(PermissionSupporter.scala:27)
at viper.silicon.rules.permissionSupporter$.$anonfun$assertNotNegative$1$adapted(PermissionSupporter.scala:26)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:300)
at viper.silicon.rules.permissionSupporter$.assertNotNegative(PermissionSupporter.scala:26)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$33(Consumer.scala:416)
at viper.silicon.rules.evaluator$.$anonfun$evalLocationAccess$1(Evaluator.scala:1251)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:163)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalLocationAccess(Evaluator.scala:1250)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$32(Consumer.scala:415)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1297)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1297)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1(Evaluator.scala:1312)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1$adapted(Evaluator.scala:1311)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:300)
at viper.silicon.rules.evaluator$.failIfDivByZero(Evaluator.scala:1311)
at viper.silicon.rules.evaluator$.$anonfun$eval2$31(Evaluator.scala:443)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$30(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:441)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1296)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1283)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:433)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1296)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1283)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:433)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.consumer$.consumeTlc(Consumer.scala:414)
at viper.silicon.rules.consumer$.$anonfun$wrappedConsumeTlc$1(Consumer.scala:164)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$1(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.tryOrFailWithResult(ExecutionFlowController.scala:118)
at viper.silicon.rules.executionFlowController$.tryOrFail2(ExecutionFlowController.scala:174)
at viper.silicon.rules.consumer$.wrappedConsumeTlc(Consumer.scala:167)
at viper.silicon.rules.consumer$.consumeTlcs(Consumer.scala:125)
at viper.silicon.rules.consumer$.$anonfun$consumeTlcs$1(Consumer.scala:126)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$3(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFailWithResult$1(ExecutionFlowController.scala:120)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$2(ExecutionFlowController.scala:174)
at viper.silicon.rules.consumer$.$anonfun$wrappedConsumeTlc$2(Consumer.scala:166)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$35(Consumer.scala:427)
at viper.silicon.rules.chunkSupporter$.$anonfun$consume$1(ChunkSupporter.scala:79)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$3(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFailWithResult$1(ExecutionFlowController.scala:120)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$2(ExecutionFlowController.scala:174)
at viper.silicon.rules.chunkSupporter$.$anonfun$consume2$4(ChunkSupporter.scala:127)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$1(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.tryOrFailWithResult(ExecutionFlowController.scala:118)
at viper.silicon.rules.executionFlowController$.tryOrFail2(ExecutionFlowController.scala:174)
at viper.silicon.rules.chunkSupporter$.consume2(ChunkSupporter.scala:134)
at viper.silicon.rules.chunkSupporter$.consume(ChunkSupporter.scala:76)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$34(Consumer.scala:424)
at viper.silicon.rules.permissionSupporter$.$anonfun$assertNotNegative$1(PermissionSupporter.scala:27)
at viper.silicon.rules.permissionSupporter$.$anonfun$assertNotNegative$1$adapted(PermissionSupporter.scala:26)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:300)
at viper.silicon.rules.permissionSupporter$.assertNotNegative(PermissionSupporter.scala:26)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$33(Consumer.scala:416)
at viper.silicon.rules.evaluator$.$anonfun$evalLocationAccess$3(Evaluator.scala:1254)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:163)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:163)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.evals(Evaluator.scala:72)
at viper.silicon.rules.evaluator$.evalLocationAccess(Evaluator.scala:1253)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$32(Consumer.scala:415)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1297)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1297)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:101)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$eval2$71(Evaluator.scala:852)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:79)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:82)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1(Evaluator.scala:1312)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1$adapted(Evaluator.scala:1311)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:300)
at viper.silicon.rules.evaluator$.failIfDivByZero(Evaluator.scala:1311)
at viper.silicon.rules.evaluator$.$anonfun$eval2$31(Evaluator.scala:443)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$30(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:441)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:756)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1296)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1283)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:433)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1296)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1283)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:433)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.consumer$.consumeTlc(Consumer.scala:414)
at viper.silicon.rules.consumer$.$anonfun$wrappedConsumeTlc$1(Consumer.scala:164)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$1(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.tryOrFailWithResult(ExecutionFlowController.scala:118)
at viper.silicon.rules.executionFlowController$.tryOrFail2(ExecutionFlowController.scala:174)
at viper.silicon.rules.consumer$.wrappedConsumeTlc(Consumer.scala:167)
at viper.silicon.rules.consumer$.consumeTlcs(Consumer.scala:125)
at viper.silicon.rules.consumer$.$anonfun$consumeTlcs$1(Consumer.scala:126)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$3(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFailWithResult$1(ExecutionFlowController.scala:120)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$2(ExecutionFlowController.scala:174)
at viper.silicon.rules.consumer$.$anonfun$wrappedConsumeTlc$2(Consumer.scala:166)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$35(Consumer.scala:427)
at viper.silicon.rules.chunkSupporter$.$anonfun$consume$1(ChunkSupporter.scala:79)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$3(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFailWithResult$1(ExecutionFlowController.scala:120)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$2(ExecutionFlowController.scala:174)
at viper.silicon.rules.chunkSupporter$.$anonfun$consume2$4(ChunkSupporter.scala:127)
at viper.silicon.rules.executionFlowController$.$anonfun$tryOrFail2$1(ExecutionFlowController.scala:174)
at viper.silicon.rules.executionFlowController$.tryOrFailWithResult(ExecutionFlowController.scala:118)
at viper.silicon.rules.executionFlowController$.tryOrFail2(ExecutionFlowController.scala:174)
at viper.silicon.rules.chunkSupporter$.consume2(ChunkSupporter.scala:134)
at viper.silicon.rules.chunkSupporter$.consume(ChunkSupporter.scala:76)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$34(Consumer.scala:424)
at viper.silicon.rules.permissionSupporter$.$anonfun$assertNotNegative$1(PermissionSupporter.scala:27)
at viper.silicon.rules.permissionSupporter$.$anonfun$assertNotNegative$1$adapted(PermissionSupporter.scala:26)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:300)
at viper.silicon.rules.permissionSupporter$.assertNotNegative(PermissionSupporter.scala:26)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$33(Consumer.scala:416)
at viper.silicon.rules.evaluator$.$anonfun$evalLocationAccess$1(Evaluator.scala:1251)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:163)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.evalLocationAccess(Evaluator.scala:1250)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$32(Consumer.scala:415)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1298)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.$anonfun$eval2$29(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:165)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.$anonfun$eval2$28(Evaluator.scala:437)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:94)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:146)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:158)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:131)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:92)
at viper.sil...
Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec ► TTTmsg case study (implementation execution) verifies with silicon
Failed test found in:
reports/ubuntu-1/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml
reports/ubuntu-2/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml
reports/ubuntu-5/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml
Error:
org.scalatest.exceptions.TestFailedException: Pass did not equal Error(choreography:resolutionError:endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor)Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Error(choreography:resolutionError:endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor)
Expected test result: pass
Actual test result: error with code choreography:resolutionError:endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor
at org.scalatest.Assertions.newAssertionFailedException(Assertions.scala:472)
at org.scalatest.Assertions.newAssertionFailedException$(Assertions.scala:471)
at org.scalatest.Assertions$.newAssertionFailedException(Assertions.scala:1231)
at org.scalatest.Assertions$AssertionsHelper.macroAssert(Assertions.scala:1295)
at vct.test.integration.helper.VeyMontSpec.processResult(VeyMontSpec.scala:222)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$4(VeyMontSpec.scala:200)
at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3(VeyMontSpec.scala:190)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3$adapted(VeyMontSpec.scala:176)
at hre.util.FilesHelper$.withTempDir(FilesHelper.scala:11)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$2(VeyMontSpec.scala:176)
at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
at org.scalatest.Transformer.apply(Transformer.scala:22)
at org.scalatest.Transformer.apply(Transformer.scala:20)
at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
at scala.collection.immutable.List.foreach(List.scala:333)
at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
at org.scalatest.Suite.run(Suite.scala:1112)
at org.scalatest.Suite.run$(Suite.scala:1094)
at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
at org.scalatest.Suite.run(Suite.scala:1109)
at org.scalatest.Suite.run$(Suite.scala:1094)
at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
at scala.collection.immutable.List.foreach(List.scala:333)
at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
at org.scalatest.tools.Runner$.main(Runner.scala:775)
at org.scalatest.tools.Runner.main(Runner.scala)
Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec ► TTT case study (choreographic verification) verifies with silicon
Failed test found in:
reports/ubuntu-5/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml
Error:
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
Internal type error: CoercionErrors must not bubble. Expression `TicTacToeAnnotations_875783153(P1_1283164732, P2_1868382440)` could not be coerced to `boolean``)
Expected test result: pass
Actual test result: crash with message:
The following error occurred during choreography verification:
Internal type error: CoercionErrors must not bubble. Expression `TicTacToeAnnotations_875783153(P1_1283164732, P2_1868382440)` could not be coerced to `boolean``
at org.scalatest.Assertions.newAssertionFailedException(Assertions.scala:472)
at org.scalatest.Assertions.newAssertionFailedException$(Assertions.scala:471)
at org.scalatest.Assertions$.newAssertionFailedException(Assertions.scala:1231)
at org.scalatest.Assertions$AssertionsHelper.macroAssert(Assertions.scala:1295)
at vct.test.integration.helper.VeyMontSpec.processResult(VeyMontSpec.scala:222)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$4(VeyMontSpec.scala:200)
at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3(VeyMontSpec.scala:190)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3$adapted(VeyMontSpec.scala:176)
at hre.util.FilesHelper$.withTempDir(FilesHelper.scala:11)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$2(VeyMontSpec.scala:176)
at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
at org.scalatest.Transformer.apply(Transformer.scala:22)
at org.scalatest.Transformer.apply(Transformer.scala:20)
at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
at scala.collection.immutable.List.foreach(List.scala:333)
at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
at org.scalatest.Suite.run(Suite.scala:1112)
at org.scalatest.Suite.run$(Suite.scala:1094)
at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
at org.scalatest.Suite.run(Suite.scala:1109)
at org.scalatest.Suite.run$(Suite.scala:1094)
at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
at scala.collection.immutable.List.foreach(List.scala:333)
at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
at org.scalatest.tools.Runner$.main(Runner.scala:775)
at org.scalatest.tools.Runner.main(Runner.scala)
Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.VeyMontExamplesSpec ► Leader elect star (generated permissions) verifies with silicon
Failed test found in:
reports/ubuntu-6/TEST-vct.test.integration.examples.veymont.VeyMontExamplesSpec.xml
Error:
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
Internal type error: CoercionErrors must not bubble. Expression `(C_137113831.N_284770129 == 0 ==>
A_1397358947.MaxVal_1325542618 == A_1397358947.Rank_2136530535 &&
B_225771694.MaxVal_1325542618 == B_225771694.Rank_2136530535 &&
C_137113831.MaxVal_1921960624 == C_137113831.Rank_1541943472 &&
D_1915529329.MaxVal_1325542618 == D_1915529329.Rank_2136530535) **
(C_137113831.N_284770129 == 1 ==>
(C_137113831.Rank_1541943472 > A_1397358947.Rank_2136530535
? A_1397358947.MaxVal_1325542618 == C_137113831.Rank_1541943472
: A_1397358947.MaxVal_1325542618 == A_1397358947.Rank_2136530535)) **
(C_137113831.N_284770129 == 1 ==>
(C_137113831.Rank_1541943472 > B_225771694.Rank_2136530535
? B_225771694.MaxVal_1325542618 == C_137113831.Rank_1541943472
: B_225771694.MaxVal_1325542618 == B_225771694.Rank_2136530535)) **
(C_137113831.N_284770129 == 1 ==>
(C_137113831.Rank_1541943472 > D_1915529329.Rank_2136530535
? D_1915529329.MaxVal_1325542618 == C_137113831.Rank_1541943472
: D_1915529329.MaxVal_1325542618 == D_1915529329.Rank_2136530535)) **
(C_137113831.N_284770129 >= 1 ==>
C_137113831.MaxVal_1921960624 ==
C_137113831.MaxVal_1065654720(
A_1397358947.Rank_2136530535,
B_225771694.Rank_2136530535,
D_1915529329.Rank_2136530535,
C_137113831.Rank_1541943472
)) **
(C_137113831.N_284770129 == 2 ==>
A_1397358947.MaxVal_1325542618 ==
C_137113831.MaxVal_1065654720(
A_1397358947.Rank_2136530535,
B_225771694.Rank_2136530535,
D_1915529329.Rank_2136530535,
C_137113831.Rank_1541943472
)) **
(C_137113831.N_284770129 == 2 ==>
B_225771694.MaxVal_1325542618 ==
C_137113831.MaxVal_1065654720(
A_1397358947.Rank_2136530535,
B_225771694.Rank_2136530535,
D_1915529329.Rank_2136530535,
C_137113831.Rank_1541943472
)) **
(C_137113831.N_284770129 == 2 ==>
D_1915529329.MaxVal_1325542618 ==
C_137113831.MaxVal_1065654720(
A_1397358947.Rank_2136530535,
B_225771694.Rank_2136530535,
D_1915529329.Rank_2136530535,
C_137113831.Rank_1541943472
)) **
A_1397358947.N_1982363227 < 2 == B_225771694.N_1982363227 < 2 **
B_225771694.N_1982363227 < 2 == D_1915529329.N_1982363227 < 2 **
D_1915529329.N_1982363227 < 2 == C_137113831.N_284770129 < 2` could not be coerced to `boolean``)
Expected test result: pass
Actual test result: crash with message:
The following error occurred during choreography verification:
Internal type error: CoercionErrors must not bubble. Expression `(C_137113831.N_284770129 == 0 ==>
A_1397358947.MaxVal_1325542618 == A_1397358947.Rank_2136530535 &&
B_225771694.MaxVal_1325542618 == B_225771694.Rank_2136530535 &&
C_137113831.MaxVal_1921960624 == C_137113831.Rank_1541943472 &&
D_1915529329.MaxVal_1325542618 == D_1915529329.Rank_2136530535) **
(C_137113831.N_284770129 == 1 ==>
(C_137113831.Rank_1541943472 > A_1397358947.Rank_2136530535
? A_1397358947.MaxVal_1325542618 == C_137113831.Rank_1541943472
: A_1397358947.MaxVal_1325542618 == A_1397358947.Rank_2136530535)) **
(C_137113831.N_284770129 == 1 ==>
(C_137113831.Rank_1541943472 > B_225771694.Rank_2136530535
? B_225771694.MaxVal_1325542618 == C_137113831.Rank_1541943472
: B_225771694.MaxVal_1325542618 == B_225771694.Rank_2136530535)) **
(C_137113831.N_284770129 == 1 ==>
(C_137113831.Rank_1541943472 > D_1915529329.Rank_2136530535
? D_1915529329.MaxVal_1325542618 == C_137113831.Rank_1541943472
: D_1915529329.MaxVal_1325542618 == D_1915529329.Rank_2136530535)) **
(C_137113831.N_284770129 >= 1 ==>
C_137113831.MaxVal_1921960624 ==
C_137113831.MaxVal_1065654720(
A_1397358947.Rank_2136530535,
B_225771694.Rank_2136530535,
D_1915529329.Rank_2136530535,
C_137113831.Rank_1541943472
)) **
(C_137113831.N_284770129 == 2 ==>
A_1397358947.MaxVal_1325542618 ==
C_137113831.MaxVal_1065654720(
A_1397358947.Rank_2136530535,
B_225771694.Rank_2136530535,
D_1915529329.Rank_2136530535,
C_137113831.Rank_1541943472
)) **
(C_137113831.N_284770129 == 2 ==>
B_225771694.MaxVal_1325542618 ==
C_137113831.MaxVal_1065654720(
A_1397358947.Rank_2136530535,
B_225771694.Rank_2136530535,
D_1915529329.Rank_2136530535,
C_137113831.Rank_1541943472
)) **
(C_137113831.N_284770129 == 2 ==>
D_1915529329.MaxVal_1325542618 ==
C_137113831.MaxVal_1065654720(
A_1397358947.Rank_2136530535,
B_225771694.Rank_2136530535,
D_1915529329.Rank_2136530535,
C_137113831.Rank_1541943472
)) **
A_1397358947.N_1982363227 < 2 == B_225771694.N_1982363227 < 2 **
B_225771694.N_1982363227 < 2 == D_1915529329.N_1982363227 < 2 **
D_1915529329.N_1982363227 < 2 == C_137113831.N_284770129 < 2` could not be coerced to `boolean``
at org.scalatest.Assertions.newAssertionFailedException(Assertions.scala:472)
at org.scalatest.Assertions.newAssertionFailedException$(Assertions.scala:471)
at org.scalatest.Assertions$.newAssertionFailedException(Assertions.scala:1231)
at org.scalatest.Assertions$AssertionsHelper.macroAssert(Assertions.scala:1295)
at vct.test.integration.helper.VeyMontSpec.processResult(VeyMontSpec.scala:222)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$4(VeyMontSpec.scala:200)
at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3(VeyMontSpec.scala:190)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3$adapted(VeyMontSpec.scala:176)
at hre.util.FilesHelper$.withTempDir(FilesHelper.scala:11)
at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$2(VeyMontSpec.scala:176)
at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
at org.scalatest.Transformer.apply(Transformer.scala:22)
at org.scalatest.Transformer.apply(Transformer.scala:20)
at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
at scala.collection.immutable.List.foreach(List.scala:333)
at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
at org.scalatest.Suite.run(Suite.scala:1112)
at org.scalatest.Suite.run$(Suite.scala:1094)
at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
at org.scalatest.Suite.run(Suite.scala:1109)
at org.scalatest.Suite.run$(Suite.scala:1094)
at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
at scala.collection.immutable.List.foreach(List.scala:333)
at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
at org.scalatest.tools.Runner$.main(Runner.scala:775)
at org.scalatest.tools.Runner.main(Runner.scala)
Loading