When i try Implies without other spec keywords, such as Ensures, Assert, Nagini reports some error messages from java. It would be better that nagini can output some error messages like "syntax error or invalid.contract.position"
Program
java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 3210 column 185: Sorts $Ref and Bool are incompatible")
at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
at viper.silicon.Silicon.verify(Silicon.scala:203)
at viper.silicon.Silicon.verify(Silicon.scala:161)
at viper.silver.frontend.DefaultFrontend.verification(Frontend.scala:270)
at viper.silver.frontend.DefaultFrontend.verification$(Frontend.scala:268)
at viper.silicon.SiliconFrontend.viper$silver$frontend$SilFrontend$$super$verification(Silicon.scala:317)
at viper.silver.frontend.SilFrontend.verification(SilFrontend.scala:267)
at viper.silver.frontend.SilFrontend.verification$(SilFrontend.scala:240)
at viper.silicon.SiliconFrontend.verification(Silicon.scala:317)
at viper.silver.frontend.DefaultPhases.$anonfun$Verification$1(Frontend.scala:117)
at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1(Frontend.scala:62)
at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1$adapted(Frontend.scala:60)
at scala.collection.immutable.List.foreach(List.scala:333)
at viper.silver.frontend.Frontend.runAllPhases(Frontend.scala:60)
at viper.silver.frontend.Frontend.runAllPhases$(Frontend.scala:59)
at viper.silicon.SiliconFrontend.runAllPhases(Silicon.scala:317)
at viper.silver.frontend.ViperFrontendAPI.verify(ViperFrontendAPI.scala:46)
at viper.silver.frontend.ViperFrontendAPI.verify$(ViperFrontendAPI.scala:41)
at viper.silicon.MinimalSiliconFrontendAPI.verify(Silicon.scala:372)
Caused by: java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 3210 column 185: Sorts $Ref and Bool are incompatible")
at java.base/java.util.concurrent.ForkJoinTask.get(ForkJoinTask.java:1006)
at viper.silicon.verifier.DefaultMainVerifier.$anonfun$verify$13(DefaultMainVerifier.scala:284)
at scala.collection.immutable.List.flatMap(List.scala:293)
at scala.collection.immutable.List.flatMap(List.scala:79)
at viper.silicon.verifier.DefaultMainVerifier.verify(DefaultMainVerifier.scala:284)
at viper.silicon.Silicon.viper$silicon$Silicon$$runVerifier(Silicon.scala:243)
at viper.silicon.Silicon$$anon$1.call(Silicon.scala:197)
at viper.silicon.Silicon$$anon$1.call(Silicon.scala:196)
at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
at java.base/java.lang.Thread.run(Thread.java:829)
Caused by: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 3210 column 185: Sorts $Ref and Bool are incompatible")
at viper.silicon.decider.ProverStdIO.readSuccess(ProverStdIO.scala:415)
at viper.silicon.decider.ProverStdIO.assume(ProverStdIO.scala:231)
at viper.silicon.decider.ProverStdIO.assume(ProverStdIO.scala:224)
at viper.silicon.decider.DefaultDeciderProvider$decider$.$anonfun$assumeWithoutSmokeChecks$3(Decider.scala:270)
at viper.silicon.decider.DefaultDeciderProvider$decider$.$anonfun$assumeWithoutSmokeChecks$3$adapted(Decider.scala:270)
at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:575)
at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:573)
at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assumeWithoutSmokeChecks(Decider.scala:270)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assume(Decider.scala:255)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assumeDefinition(Decider.scala:245)
at viper.silicon.rules.executor$.ssaifyRhs(Executor.scala:688)
at viper.silicon.rules.executor$.$anonfun$exec2$3(Executor.scala:354)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$eval2$17(Evaluator.scala:334)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:97)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:75)
at viper.silicon.rules.evaluator$.evalImplies(Evaluator.scala:1139)
at viper.silicon.rules.evaluator$.$anonfun$eval2$16(Evaluator.scala:332)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:97)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:75)
at viper.silicon.rules.evaluator$.$anonfun$eval2$70(Evaluator.scala:817)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:97)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:75)
at viper.silicon.rules.evaluator$.$anonfun$eval2$70(Evaluator.scala:817)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:157)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:721)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:162)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:721)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:331)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.executor$.exec2(Executor.scala:353)
at viper.silicon.rules.executor$.exec(Executor.scala:314)
at viper.silicon.rules.executor$.execs(Executor.scala:305)
at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:306)
at viper.silicon.rules.executor$.$anonfun$exec$24(Executor.scala:316)
at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:325)
at viper.silicon.rules.executor$.$anonfun$exec2$3(Executor.scala:355)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:162)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.executor$.exec2(Executor.scala:353)
at viper.silicon.rules.executor$.exec(Executor.scala:314)
at viper.silicon.rules.executor$.execs(Executor.scala:305)
at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:306)
at viper.silicon.rules.executor$.$anonfun$exec$24(Executor.scala:316)
at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:325)
at viper.silicon.rules.executor$.$anonfun$exec2$3(Executor.scala:355)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:156)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.executor$.exec2(Executor.scala:353)
at viper.silicon.rules.executor$.exec(Executor.scala:314)
at viper.silicon.rules.executor$.execs(Executor.scala:305)
at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:306)
at viper.silicon.rules.executor$.$anonfun$exec$24(Executor.scala:316)
at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:325)
at viper.silicon.rules.executor$.$anonfun$exec2$3(Executor.scala:355)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:156)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.executor$.exec2(Executor.scala:353)
at viper.silicon.rules.executor$.exec(Executor.scala:314)
at viper.silicon.rules.executor$.execs(Executor.scala:305)
at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:306)
at viper.silicon.rules.executor$.$anonfun$exec$24(Executor.scala:316)
at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:325)
at viper.silicon.rules.executor$.$anonfun$exec2$3(Executor.scala:355)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:920)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.executor$.exec2(Executor.scala:353)
at viper.silicon.rules.executor$.exec(Executor.scala:314)
at viper.silicon.rules.executor$.execs(Executor.scala:305)
at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:306)
at viper.silicon.rules.executor$.$anonfun$exec$24(Executor.scala:316)
at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:325)
at viper.silicon.rules.executor$.exec2(Executor.scala:350)
at viper.silicon.rules.executor$.exec(Executor.scala:314)
at viper.silicon.rules.executor$.execs(Executor.scala:305)
at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:306)
at viper.silicon.rules.executor$.$anonfun$exec$24(Executor.scala:316)
at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:325)
at viper.silicon.rules.executor$.exec2(Executor.scala:350)
at viper.silicon.rules.executor$.exec(Executor.scala:314)
at viper.silicon.rules.executor$.execs(Executor.scala:305)
at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:306)
at viper.silicon.rules.executor$.$anonfun$exec$24(Executor.scala:316)
at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:325)
at viper.silicon.rules.executor$.exec2(Executor.scala:350)
at viper.silicon.rules.executor$.exec(Executor.scala:314)
at viper.silicon.rules.executor$.execs(Executor.scala:305)
at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:306)
at viper.silicon.rules.executor$.$anonfun$exec$24(Executor.scala:316)
at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:325)
at viper.silicon.rules.executor$.exec2(Executor.scala:350)
at viper.silicon.rules.executor$.exec(Executor.scala:314)
at viper.silicon.rules.executor$.execs(Executor.scala:305)
at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:306)
at viper.silicon.rules.executor$.$anonfun$exec$24(Executor.scala:316)
at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:325)
at viper.silicon.rules.executor$.exec2(Executor.scala:350)
at viper.silicon.rules.executor$.exec(Executor.scala:314)
at viper.silicon.rules.executor$.execs(Executor.scala:305)
at viper.silicon.rules.executor$.exec(Executor.scala:207)
at viper.silicon.rules.executor$.exec(Executor.scala:198)
at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$16(MethodSupporter.scala:113)
at viper.silicon.rules.executionFlowController$.$anonfun$locally$1(ExecutionFlowController.scala:99)
at viper.silicon.rules.executionFlowController$.locallyWithResult(ExecutionFlowController.scala:62)
at viper.silicon.rules.executionFlowController$.locally(ExecutionFlowController.scala:99)
at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$15(MethodSupporter.scala:112)
at viper.silicon.interfaces.NonFatalResult.$amp$amp(Verification.scala:81)
at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$11(MethodSupporter.scala:112)
at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:199)
at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:214)
at viper.silicon.rules.producer$.$anonfun$produceTlc$55(Producer.scala:507)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:153)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.producer$.produceTlc(Producer.scala:505)
at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:197)
at viper.silicon.rules.producer$.produceTlcs(Producer.scala:146)
at viper.silicon.rules.producer$.$anonfun$produceTlcs$1(Producer.scala:158)
at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:199)
at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:214)
at viper.silicon.rules.producer$.$anonfun$produceTlc$55(Producer.scala:507)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:97)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:75)
at viper.silicon.rules.evaluator$.$anonfun$eval2$70(Evaluator.scala:817)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:97)
at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:42)
at viper.silicon.rules.joiner$.join(Joiner.scala:75)
at viper.silicon.rules.evaluator$.$anonfun$eval2$70(Evaluator.scala:817)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:157)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:721)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:162)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:721)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.producer$.produceTlc(Producer.scala:505)
at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:197)
at viper.silicon.rules.producer$.produceTlcs(Producer.scala:157)
at viper.silicon.rules.producer$.$anonfun$produceTlcs$1(Producer.scala:158)
at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:199)
at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:214)
at viper.silicon.rules.producer$.$anonfun$produceTlc$55(Producer.scala:507)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$eval2$34(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$eval2$34(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.evals(Evaluator.scala:71)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$eval2$34(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:162)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.evals(Evaluator.scala:71)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.evals(Evaluator.scala:71)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.producer$.produceTlc(Producer.scala:505)
at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:197)
at viper.silicon.rules.producer$.produceTlcs(Producer.scala:157)
at viper.silicon.rules.producer$.$anonfun$produceTlcs$1(Producer.scala:158)
at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:199)
at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:214)
at viper.silicon.rules.producer$.$anonfun$produceTlc$55(Producer.scala:507)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$eval2$34(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$eval2$34(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.evals(Evaluator.scala:71)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$eval2$34(Evaluator.scala:442)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:162)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.evals(Evaluator.scala:71)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.evals(Evaluator.scala:71)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:438)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.producer$.produceTlc(Producer.scala:505)
at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:197)
at viper.silicon.rules.producer$.produceTlcs(Producer.scala:157)
at viper.silicon.rules.producer$.$anonfun$produceTlcs$1(Producer.scala:158)
at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:199)
at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:214)
at viper.silicon.rules.producer$.$anonfun$produceTlc$55(Producer.scala:507)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1241)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:156)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1240)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:162)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1239)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:160)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.producer$.produceTlc(Producer.scala:505)
at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:197)
at viper.silicon.rules.producer$.produceTlcs(Producer.scala:157)
at viper.silicon.rules.producer$.produces(Producer.scala:128)
at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$9(MethodSupporter.scala:101)
at viper.silicon.rules.executionFlowController$.$anonfun$locally$1(ExecutionFlowController.scala:99)
at viper.silicon.rules.executionFlowController$.locallyWithResult(ExecutionFlowController.scala:62)
at viper.silicon.rules.executionFlowController$.locally(ExecutionFlowController.scala:99)
at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.verify(MethodSupporter.scala:100)
at viper.silicon.verifier.DefaultMainVerifier.$anonfun$verify$8(DefaultMainVerifier.scala:259)
at viper.silicon.verifier.VerificationPoolManager$WorkerAwareForkJoinTask.compute(VerificationPoolManager.scala:151)
at viper.silicon.verifier.VerificationPoolManager$WorkerAwareForkJoinTask.compute(VerificationPoolManager.scala:144)
at java.base/java.util.concurrent.RecursiveTask.exec(RecursiveTask.java:94)
at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:290)
at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1020)
at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1656)
at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1594)
at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:183)
Traceback (most recent call last):
File "ForkJoinWorkerThread.java", line 183, in java.util.concurrent.ForkJoinWorkerThread.run
File "ForkJoinPool.java", line 1594, in java.util.concurrent.ForkJoinPool.runWorker
File "ForkJoinPool.java", line 1656, in java.util.concurrent.ForkJoinPool.scan
File "ForkJoinPool.java", line 1020, in java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec
File "ForkJoinTask.java", line 290, in java.util.concurrent.ForkJoinTask.doExec
File "RecursiveTask.java", line 94, in java.util.concurrent.RecursiveTask.exec
File "VerificationPoolManager.scala", line 144, in viper.silicon.verifier.VerificationPoolManager$WorkerAwareForkJoinTask.compute
File "VerificationPoolManager.scala", line 151, in viper.silicon.verifier.VerificationPoolManager$WorkerAwareForkJoinTask.compute
File "DefaultMainVerifier.scala", line 259, in viper.silicon.verifier.DefaultMainVerifier.$anonfun$verify$8
File "MethodSupporter.scala", line 100, in viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.verify
File "ExecutionFlowController.scala", line 99, in viper.silicon.rules.executionFlowController$.locally
File "ExecutionFlowController.scala", line 62, in viper.silicon.rules.executionFlowController$.locallyWithResult
File "ExecutionFlowController.scala", line 99, in viper.silicon.rules.executionFlowController$.$anonfun$locally$1
File "MethodSupporter.scala", line 101, in viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$9
File "Producer.scala", line 128, in viper.silicon.rules.producer$.produces
File "Producer.scala", line 157, in viper.silicon.rules.producer$.produceTlcs
File "Producer.scala", line 197, in viper.silicon.rules.producer$.wrappedProduceTlc
File "Producer.scala", line 505, in viper.silicon.rules.producer$.produceTlc
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 160, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 1239, in viper.silicon.rules.evaluator$.evalBinOp
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 162, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 1240, in viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 156, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 1241, in viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Producer.scala", line 507, in viper.silicon.rules.producer$.$anonfun$produceTlc$55
File "Producer.scala", line 214, in viper.silicon.rules.producer$.$anonfun$produceTlc$1
File "Producer.scala", line 199, in viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1
File "Producer.scala", line 158, in viper.silicon.rules.producer$.$anonfun$produceTlcs$1
File "Producer.scala", line 157, in viper.silicon.rules.producer$.produceTlcs
File "Producer.scala", line 197, in viper.silicon.rules.producer$.wrappedProduceTlc
File "Producer.scala", line 505, in viper.silicon.rules.producer$.produceTlc
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 438, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 71, in viper.silicon.rules.evaluator$.evals
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 438, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 71, in viper.silicon.rules.evaluator$.evals
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 162, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 78, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 442, in viper.silicon.rules.evaluator$.$anonfun$eval2$34
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 438, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 71, in viper.silicon.rules.evaluator$.evals
File "Evaluator.scala", line 78, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 442, in viper.silicon.rules.evaluator$.$anonfun$eval2$34
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 78, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 442, in viper.silicon.rules.evaluator$.$anonfun$eval2$34
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Producer.scala", line 507, in viper.silicon.rules.producer$.$anonfun$produceTlc$55
File "Producer.scala", line 214, in viper.silicon.rules.producer$.$anonfun$produceTlc$1
File "Producer.scala", line 199, in viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1
File "Producer.scala", line 158, in viper.silicon.rules.producer$.$anonfun$produceTlcs$1
File "Producer.scala", line 157, in viper.silicon.rules.producer$.produceTlcs
File "Producer.scala", line 197, in viper.silicon.rules.producer$.wrappedProduceTlc
File "Producer.scala", line 505, in viper.silicon.rules.producer$.produceTlc
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 438, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 71, in viper.silicon.rules.evaluator$.evals
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 438, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 71, in viper.silicon.rules.evaluator$.evals
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 162, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 78, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 442, in viper.silicon.rules.evaluator$.$anonfun$eval2$34
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 438, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 71, in viper.silicon.rules.evaluator$.evals
File "Evaluator.scala", line 78, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 442, in viper.silicon.rules.evaluator$.$anonfun$eval2$34
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 78, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 442, in viper.silicon.rules.evaluator$.$anonfun$eval2$34
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Producer.scala", line 507, in viper.silicon.rules.producer$.$anonfun$produceTlc$55
File "Producer.scala", line 214, in viper.silicon.rules.producer$.$anonfun$produceTlc$1
File "Producer.scala", line 199, in viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1
File "Producer.scala", line 158, in viper.silicon.rules.producer$.$anonfun$produceTlcs$1
File "Producer.scala", line 157, in viper.silicon.rules.producer$.produceTlcs
File "Producer.scala", line 197, in viper.silicon.rules.producer$.wrappedProduceTlc
File "Producer.scala", line 505, in viper.silicon.rules.producer$.produceTlc
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 721, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 162, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 721, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 157, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 78, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 817, in viper.silicon.rules.evaluator$.$anonfun$eval2$70
File "Joiner.scala", line 75, in viper.silicon.rules.joiner$.join
File "Verification.scala", line 42, in viper.silicon.interfaces.VerificationResult.combine
File "Joiner.scala", line 97, in viper.silicon.rules.joiner$.$anonfun$join$3
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 78, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 817, in viper.silicon.rules.evaluator$.$anonfun$eval2$70
File "Joiner.scala", line 75, in viper.silicon.rules.joiner$.join
File "Verification.scala", line 42, in viper.silicon.interfaces.VerificationResult.combine
File "Joiner.scala", line 97, in viper.silicon.rules.joiner$.$anonfun$join$3
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Producer.scala", line 507, in viper.silicon.rules.producer$.$anonfun$produceTlc$55
File "Producer.scala", line 214, in viper.silicon.rules.producer$.$anonfun$produceTlc$1
File "Producer.scala", line 199, in viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1
File "Producer.scala", line 158, in viper.silicon.rules.producer$.$anonfun$produceTlcs$1
File "Producer.scala", line 146, in viper.silicon.rules.producer$.produceTlcs
File "Producer.scala", line 197, in viper.silicon.rules.producer$.wrappedProduceTlc
File "Producer.scala", line 505, in viper.silicon.rules.producer$.produceTlc
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 153, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Producer.scala", line 507, in viper.silicon.rules.producer$.$anonfun$produceTlc$55
File "Producer.scala", line 214, in viper.silicon.rules.producer$.$anonfun$produceTlc$1
File "Producer.scala", line 199, in viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1
File "MethodSupporter.scala", line 112, in viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$11
File "Verification.scala", line 81, in viper.silicon.interfaces.NonFatalResult.$amp$amp
File "MethodSupporter.scala", line 112, in viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$15
File "ExecutionFlowController.scala", line 99, in viper.silicon.rules.executionFlowController$.locally
File "ExecutionFlowController.scala", line 62, in viper.silicon.rules.executionFlowController$.locallyWithResult
File "ExecutionFlowController.scala", line 99, in viper.silicon.rules.executionFlowController$.$anonfun$locally$1
File "MethodSupporter.scala", line 113, in viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$16
File "Executor.scala", line 198, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 207, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 305, in viper.silicon.rules.executor$.execs
File "Executor.scala", line 314, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 350, in viper.silicon.rules.executor$.exec2
File "Executor.scala", line 325, in viper.silicon.rules.executor$.$anonfun$exec2$1
File "Executor.scala", line 316, in viper.silicon.rules.executor$.$anonfun$exec$24
File "Executor.scala", line 306, in viper.silicon.rules.executor$.$anonfun$execs$1
File "Executor.scala", line 305, in viper.silicon.rules.executor$.execs
File "Executor.scala", line 314, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 350, in viper.silicon.rules.executor$.exec2
File "Executor.scala", line 325, in viper.silicon.rules.executor$.$anonfun$exec2$1
File "Executor.scala", line 316, in viper.silicon.rules.executor$.$anonfun$exec$24
File "Executor.scala", line 306, in viper.silicon.rules.executor$.$anonfun$execs$1
File "Executor.scala", line 305, in viper.silicon.rules.executor$.execs
File "Executor.scala", line 314, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 350, in viper.silicon.rules.executor$.exec2
File "Executor.scala", line 325, in viper.silicon.rules.executor$.$anonfun$exec2$1
File "Executor.scala", line 316, in viper.silicon.rules.executor$.$anonfun$exec$24
File "Executor.scala", line 306, in viper.silicon.rules.executor$.$anonfun$execs$1
File "Executor.scala", line 305, in viper.silicon.rules.executor$.execs
File "Executor.scala", line 314, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 350, in viper.silicon.rules.executor$.exec2
File "Executor.scala", line 325, in viper.silicon.rules.executor$.$anonfun$exec2$1
File "Executor.scala", line 316, in viper.silicon.rules.executor$.$anonfun$exec$24
File "Executor.scala", line 306, in viper.silicon.rules.executor$.$anonfun$execs$1
File "Executor.scala", line 305, in viper.silicon.rules.executor$.execs
File "Executor.scala", line 314, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 350, in viper.silicon.rules.executor$.exec2
File "Executor.scala", line 325, in viper.silicon.rules.executor$.$anonfun$exec2$1
File "Executor.scala", line 316, in viper.silicon.rules.executor$.$anonfun$exec$24
File "Executor.scala", line 306, in viper.silicon.rules.executor$.$anonfun$execs$1
File "Executor.scala", line 305, in viper.silicon.rules.executor$.execs
File "Executor.scala", line 314, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 353, in viper.silicon.rules.executor$.exec2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 920, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Executor.scala", line 355, in viper.silicon.rules.executor$.$anonfun$exec2$3
File "Executor.scala", line 325, in viper.silicon.rules.executor$.$anonfun$exec2$1
File "Executor.scala", line 316, in viper.silicon.rules.executor$.$anonfun$exec$24
File "Executor.scala", line 306, in viper.silicon.rules.executor$.$anonfun$execs$1
File "Executor.scala", line 305, in viper.silicon.rules.executor$.execs
File "Executor.scala", line 314, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 353, in viper.silicon.rules.executor$.exec2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 156, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Executor.scala", line 355, in viper.silicon.rules.executor$.$anonfun$exec2$3
File "Executor.scala", line 325, in viper.silicon.rules.executor$.$anonfun$exec2$1
File "Executor.scala", line 316, in viper.silicon.rules.executor$.$anonfun$exec$24
File "Executor.scala", line 306, in viper.silicon.rules.executor$.$anonfun$execs$1
File "Executor.scala", line 305, in viper.silicon.rules.executor$.execs
File "Executor.scala", line 314, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 353, in viper.silicon.rules.executor$.exec2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 156, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Executor.scala", line 355, in viper.silicon.rules.executor$.$anonfun$exec2$3
File "Executor.scala", line 325, in viper.silicon.rules.executor$.$anonfun$exec2$1
File "Executor.scala", line 316, in viper.silicon.rules.executor$.$anonfun$exec$24
File "Executor.scala", line 306, in viper.silicon.rules.executor$.$anonfun$execs$1
File "Executor.scala", line 305, in viper.silicon.rules.executor$.execs
File "Executor.scala", line 314, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 353, in viper.silicon.rules.executor$.exec2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 162, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Executor.scala", line 355, in viper.silicon.rules.executor$.$anonfun$exec2$3
File "Executor.scala", line 325, in viper.silicon.rules.executor$.$anonfun$exec2$1
File "Executor.scala", line 316, in viper.silicon.rules.executor$.$anonfun$exec$24
File "Executor.scala", line 306, in viper.silicon.rules.executor$.$anonfun$execs$1
File "Executor.scala", line 305, in viper.silicon.rules.executor$.execs
File "Executor.scala", line 314, in viper.silicon.rules.executor$.exec
File "Executor.scala", line 353, in viper.silicon.rules.executor$.exec2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 331, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 721, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 162, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 721, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 80, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 91, in viper.silicon.rules.evaluator$.eval
File "Evaluator.scala", line 130, in viper.silicon.rules.evaluator$.eval3
File "Evaluator.scala", line 157, in viper.silicon.rules.evaluator$.eval2
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 78, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 817, in viper.silicon.rules.evaluator$.$anonfun$eval2$70
File "Joiner.scala", line 75, in viper.silicon.rules.joiner$.join
File "Verification.scala", line 42, in viper.silicon.interfaces.VerificationResult.combine
File "Joiner.scala", line 97, in viper.silicon.rules.joiner$.$anonfun$join$3
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 81, in viper.silicon.rules.evaluator$.$anonfun$evals2$1
File "Evaluator.scala", line 78, in viper.silicon.rules.evaluator$.evals2
File "Evaluator.scala", line 817, in viper.silicon.rules.evaluator$.$anonfun$eval2$70
File "Joiner.scala", line 75, in viper.silicon.rules.joiner$.join
File "Verification.scala", line 42, in viper.silicon.interfaces.VerificationResult.combine
File "Joiner.scala", line 97, in viper.silicon.rules.joiner$.$anonfun$join$3
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Evaluator.scala", line 332, in viper.silicon.rules.evaluator$.$anonfun$eval2$16
File "Evaluator.scala", line 1139, in viper.silicon.rules.evaluator$.evalImplies
File "Joiner.scala", line 75, in viper.silicon.rules.joiner$.join
File "Verification.scala", line 42, in viper.silicon.interfaces.VerificationResult.combine
File "Joiner.scala", line 97, in viper.silicon.rules.joiner$.$anonfun$join$3
File "Evaluator.scala", line 334, in viper.silicon.rules.evaluator$.$anonfun$eval2$17
File "Evaluator.scala", line 145, in viper.silicon.rules.evaluator$.$anonfun$eval3$3
File "Evaluator.scala", line 93, in viper.silicon.rules.evaluator$.$anonfun$eval$1
File "Executor.scala", line 354, in viper.silicon.rules.executor$.$anonfun$exec2$3
File "Executor.scala", line 688, in viper.silicon.rules.executor$.ssaifyRhs
File "Decider.scala", line 245, in viper.silicon.decider.DefaultDeciderProvider$decider$.assumeDefinition
File "Decider.scala", line 255, in viper.silicon.decider.DefaultDeciderProvider$decider$.assume
File "Decider.scala", line 270, in viper.silicon.decider.DefaultDeciderProvider$decider$.assumeWithoutSmokeChecks
File "Iterable.scala", line 933, in scala.collection.AbstractIterable.foreach
File "IterableOnce.scala", line 573, in scala.collection.IterableOnceOps.foreach$
File "IterableOnce.scala", line 575, in scala.collection.IterableOnceOps.foreach
File "Decider.scala", line 270, in viper.silicon.decider.DefaultDeciderProvider$decider$.$anonfun$assumeWithoutSmokeChecks$3$adapted
File "Decider.scala", line 270, in viper.silicon.decider.DefaultDeciderProvider$decider$.$anonfun$assumeWithoutSmokeChecks$3
File "ProverStdIO.scala", line 224, in viper.silicon.decider.ProverStdIO.assume
File "ProverStdIO.scala", line 231, in viper.silicon.decider.ProverStdIO.assume
File "ProverStdIO.scala", line 415, in viper.silicon.decider.ProverStdIO.readSuccess
viper.silicon.reporting.viper.silicon.reporting.ProverInteractionFailed: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 3210 column 185: Sorts $Ref and Bool are incompatible")
The above exception was the direct cause of the following exception:
Traceback (most recent call last):
File "Thread.java", line 829, in java.lang.Thread.run
File "ThreadPoolExecutor.java", line 628, in java.util.concurrent.ThreadPoolExecutor$Worker.run
File "ThreadPoolExecutor.java", line 1128, in java.util.concurrent.ThreadPoolExecutor.runWorker
File "FutureTask.java", line 264, in java.util.concurrent.FutureTask.run
File "Silicon.scala", line 196, in viper.silicon.Silicon$$anon$1.call
File "Silicon.scala", line 197, in viper.silicon.Silicon$$anon$1.call
File "Silicon.scala", line 243, in viper.silicon.Silicon.viper$silicon$Silicon$$runVerifier
File "DefaultMainVerifier.scala", line 284, in viper.silicon.verifier.DefaultMainVerifier.verify
File "List.scala", line 79, in scala.collection.immutable.List.flatMap
File "List.scala", line 293, in scala.collection.immutable.List.flatMap
File "DefaultMainVerifier.scala", line 284, in viper.silicon.verifier.DefaultMainVerifier.$anonfun$verify$13
File "ForkJoinTask.java", line 1006, in java.util.concurrent.ForkJoinTask.get
java.util.concurrent.java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 3210 column 185: Sorts $Ref and Bool are incompatible")
The above exception was the direct cause of the following exception:
Traceback (most recent call last):
File "Silicon.scala", line 372, in viper.silicon.MinimalSiliconFrontendAPI.verify
File "ViperFrontendAPI.scala", line 41, in viper.silver.frontend.ViperFrontendAPI.verify$
File "ViperFrontendAPI.scala", line 46, in viper.silver.frontend.ViperFrontendAPI.verify
File "Silicon.scala", line 317, in viper.silicon.SiliconFrontend.runAllPhases
File "Frontend.scala", line 59, in viper.silver.frontend.Frontend.runAllPhases$
File "Frontend.scala", line 60, in viper.silver.frontend.Frontend.runAllPhases
File "List.scala", line 333, in scala.collection.immutable.List.foreach
File "Frontend.scala", line 60, in viper.silver.frontend.Frontend.$anonfun$runAllPhases$1$adapted
File "Frontend.scala", line 62, in viper.silver.frontend.Frontend.$anonfun$runAllPhases$1
File "Frontend.scala", line 117, in viper.silver.frontend.DefaultPhases.$anonfun$Verification$1
File "Silicon.scala", line 317, in viper.silicon.SiliconFrontend.verification
File "SilFrontend.scala", line 240, in viper.silver.frontend.SilFrontend.verification$
File "SilFrontend.scala", line 267, in viper.silver.frontend.SilFrontend.verification
File "Silicon.scala", line 317, in viper.silicon.SiliconFrontend.viper$silver$frontend$SilFrontend$$super$verification
File "Frontend.scala", line 268, in viper.silver.frontend.DefaultFrontend.verification$
File "Frontend.scala", line 270, in viper.silver.frontend.DefaultFrontend.verification
File "Silicon.scala", line 161, in viper.silicon.Silicon.verify
File "Silicon.scala", line 203, in viper.silicon.Silicon.verify
File "FutureTask.java", line 191, in java.util.concurrent.FutureTask.get
File "FutureTask.java", line 122, in java.util.concurrent.FutureTask.report
Exception: Java Exception
The above exception was the direct cause of the following exception:
Traceback (most recent call last):
File "/home/xx/anaconda3/envs/nagini/lib/python3.9/site-packages/nagini_translation/main.py", line 210, in verify
vresult = verifier.verify(modules, prog, arp=arp, sif=sif)
File "/home/xx/anaconda3/envs/nagini/lib/python3.9/site-packages/nagini_translation/verifier.py", line 136, in verify
result = self.silicon.verify(prog)
java.util.concurrent.java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 3210 column 185: Sorts $Ref and Bool are incompatible")
Traceback (most recent call last):
File "/home/xx/anaconda3/envs/nagini/bin/nagini", line 8, in <module>
sys.exit(main())
File "/home/xx/anaconda3/envs/nagini/lib/python3.9/site-packages/nagini_translation/main.py", line 397, in main
success = translate_and_verify(args.python_file, jvm, args, arp=args.arp, base_dir=args.base_dir)
File "/home/xx/anaconda3/envs/nagini/lib/python3.9/site-packages/nagini_translation/main.py", line 451, in translate_and_verify
print(vresult.to_string(args.ide_mode, args.show_viper_errors))
AttributeError: 'NoneType' object has no attribute 'to_string'
When i try Implies without other spec keywords, such as Ensures, Assert, Nagini reports some error messages from java. It would be better that nagini can output some error messages like "syntax error or invalid.contract.position"
Program
Error messages