"Directly" checking whether an element is in a dict results in a logic instead of type error

[dnezam]

The following program results in a logic error, even though a type error (perhaps suggesting x in domain(d)) would be expected:

package pkg

ghost
// Instead of the following type error, the program results in a logic error:
// "Logic error: expected a sequence or (multi)set type, but got dict[int°]int°°"
//:: ExpectedOutput(type_error)
requires x in d
decreases
func foo(d dict[int]int, x int) {}

Output:

Gobra 1.1-SNAPSHOT (529d2a49@(detached))
(c) Copyright ETH Zurich 2012 - 2022
12:18:47.852 [main] INFO viper.gobra.Gobra - Verifying package .. - pkg [12:18:47]
12:18:49.019 [main] ERROR viper.gobra.GobraRunner$ - An assumption was violated during execution.
12:18:49.023 [main] ERROR viper.gobra.GobraRunner$ - Logic error: expected a sequence or (multi)set type, but got dict[int°]int°°
viper.gobra.util.Violation$LogicException: Logic error: expected a sequence or (multi)set type, but got dict[int°]int°°
	at viper.gobra.util.Violation$.violation(Violation.scala:27)
	at viper.gobra.frontend.Desugar$Desugarer.$anonfun$ghostExprD$23(Desugar.scala:4279)
	at viper.gobra.util.DesugarWriter$Writer.map(DesugarWriter.scala:48)
	at viper.gobra.frontend.Desugar$Desugarer.$anonfun$ghostExprD$22(Desugar.scala:4274)
	at viper.gobra.util.DesugarWriter$Writer.flatMap(DesugarWriter.scala:54)
	at viper.gobra.frontend.Desugar$Desugarer.ghostExprD(Desugar.scala:4273)
	at viper.gobra.frontend.Desugar$Desugarer.exprD(Desugar.scala:2723)
	at viper.gobra.frontend.Desugar$Desugarer.assertionD(Desugar.scala:4555)
	at viper.gobra.frontend.Desugar$Desugarer.specificationD(Desugar.scala:4445)
	at viper.gobra.frontend.Desugar$Desugarer.preconditionD(Desugar.scala:4451)
	at viper.gobra.frontend.Desugar$Desugarer.$anonfun$functionMemberOrLitD$13(Desugar.scala:645)
	at scala.collection.immutable.Vector1.map(Vector.scala:1911)
	at scala.collection.immutable.Vector1.map(Vector.scala:377)
	at viper.gobra.frontend.Desugar$Desugarer.functionMemberOrLitD(Desugar.scala:645)
	at viper.gobra.frontend.Desugar$Desugarer.functionD(Desugar.scala:572)
	at viper.gobra.frontend.Desugar$Desugarer.registerFunction(Desugar.scala:3628)
	at viper.gobra.frontend.Desugar$Desugarer.$anonfun$packageD$1(Desugar.scala:427)
	at scala.collection.StrictOptimizedIterableOps.flatMap(StrictOptimizedIterableOps.scala:118)
	at scala.collection.StrictOptimizedIterableOps.flatMap$(StrictOptimizedIterableOps.scala:105)
	at scala.collection.immutable.Vector.flatMap(Vector.scala:113)
	at viper.gobra.frontend.Desugar$Desugarer.packageD(Desugar.scala:419)
	at viper.gobra.frontend.Desugar$.$anonfun$desugar$3(Desugar.scala:59)
	at scala.concurrent.Future$.$anonfun$apply$1(Future.scala:678)
	at scala.concurrent.impl.Promise$Transformation.run(Promise.scala:467)
	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)
java.util.concurrent.RejectedExecutionException: Task Future(<not completed>) rejected from java.util.concurrent.ThreadPoolExecutor@22969c78[Shutting down, pool size = 1, active threads = 1, queued tasks = 0, completed tasks = 34]
	at java.base/java.util.concurrent.ThreadPoolExecutor$AbortPolicy.rejectedExecution(ThreadPoolExecutor.java:2055)
	at java.base/java.util.concurrent.ThreadPoolExecutor.reject(ThreadPoolExecutor.java:825)
	at java.base/java.util.concurrent.ThreadPoolExecutor.execute(ThreadPoolExecutor.java:1355)
	at scala.concurrent.impl.ExecutionContextImpl.execute(ExecutionContextImpl.scala:21)
	at viper.server.core.DefaultVerificationExecutionContext.execute(VerificationExecutionContext.scala:67)
	at scala.concurrent.impl.Promise$Transformation.submitWithValue(Promise.scala:429)
	at scala.concurrent.impl.Promise$DefaultPromise.submitWithValue(Promise.scala:338)
	at scala.concurrent.impl.Promise$DefaultPromise.tryComplete0(Promise.scala:285)
	at scala.concurrent.impl.Promise$Transformation.run(Promise.scala:504)
	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)

[jcp19]

duplicate of #707