Appending to a slice of a struct

[rayman2000]

It looks like appending a struct to a slice crashes Gobra. I was trying stuff out and the Gobra IDE kept crashing. I reduced it down to this fairly simple example.

type MyType struct {
	x int
}

func myFunc() {
	mySlice := make([]MyType, 0)
	append(perm(1/2), mySlice, MyType{1})
}

Should this be a supported? If so we should fix it. If not then we should somehow have a more graceful way of failing.

Error message in the IDE:

An exception occurred during execution of Gobra: 
java.lang.ClassCastException: class viper.gobra.ast.internal.Old cannot be cast to class viper.gobra.ast.internal.Location
(viper.gobra.ast.internal.Old and viper.gobra.ast.internal.Location are in unnamed module of loader 'app')

Running Gobra manually gives the long and fairly unhelpful (at least for me) stacktrace:

[info] An unknown Exception was thrown.
[info] java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 2161 column 312: unknown constant ShStructget0of1<Ref> (Tuple1<Int>) 
[info] java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 2161 column 312: unknown constant ShStructget0of1<Ref> (Tuple1<Int>) 
[info]  at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
[info]  at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
[info]  at viper.silicon.Silicon.verify(Silicon.scala:202)
[info]  at viper.silicon.Silicon.verify(Silicon.scala:160)
[info]  at viper.gobra.backend.Silicon.$anonfun$verify$1(Silicon.scala:27)
[info]  at scala.concurrent.Future$.$anonfun$apply$1(Future.scala:672)
[info]  at scala.concurrent.impl.Promise$Transformation.run(Promise.scala:431)
[info]  at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
[info]  at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
[info]  at java.base/java.lang.Thread.run(Thread.java:829)
[info] Caused by: java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 2161 column 312: unknown constant ShStructget0of1<Ref> (Tuple1<Int>) 
[info]  at java.base/java.util.concurrent.ForkJoinTask.get(ForkJoinTask.java:1006)
[info]  at viper.silicon.verifier.DefaultMainVerifier.$anonfun$verify$13(DefaultMainVerifier.scala:275)
[info]  at scala.collection.immutable.List.flatMap(List.scala:293)
[info]  at scala.collection.immutable.List.flatMap(List.scala:79)
[info]  at viper.silicon.verifier.DefaultMainVerifier.verify(DefaultMainVerifier.scala:275)
[info]  at viper.silicon.Silicon.viper$silicon$Silicon$$runVerifier(Silicon.scala:242)
[info]  at viper.silicon.Silicon$$anon$1.call(Silicon.scala:196)
[info]  at viper.silicon.Silicon$$anon$1.call(Silicon.scala:195)
[info]  at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
[info]  ... 3 common frames omitted
[info] Caused by: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 2161 column 312: unknown constant ShStructget0of1<Ref> (Tuple1<Int>) 
[info]  at viper.silicon.decider.ProverStdIO.readSuccess(ProverStdIO.scala:394)
[info]  at viper.silicon.decider.ProverStdIO.assertUsingPushPop(ProverStdIO.scala:246)
[info]  at viper.silicon.decider.ProverStdIO.assert(ProverStdIO.scala:232)
[info]  at viper.silicon.decider.ProverStdIO.assert(ProverStdIO.scala:225)
[info]  at viper.silicon.decider.DefaultDeciderProvider$decider$.proverAssert(Decider.scala:284)
[info]  at viper.silicon.decider.DefaultDeciderProvider$decider$.deciderAssert(Decider.scala:266)
[info]  at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:247)
[info]  at viper.silicon.rules.evaluator$.$anonfun$eval2$4(Evaluator.scala:249)
[...]
[info]  at viper.silicon.verifier.VerificationPoolManager$WorkerAwareForkJoinTask.compute(VerificationPoolManager.scala:141)
[info]  at java.base/java.util.concurrent.RecursiveTask.exec(RecursiveTask.java:94)
[info]  at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:290)
[info]  at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1020)
[info]  at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1656)
[info]  at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1594)
[info]  at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:183)
[info] Writing report to .gobra/stats.json
[info] Could not write to the file .gobra/stats.json. Check whether the permissions to the file allow writing to it.
[info] The verification of member .. - error.myFunc() did not terminate
[info] 
[error] Nonzero exit code returned from runner: 1
[error] (Compile / run) Nonzero exit code returned from runner: 1
[error] Total time: 8 s, completed Feb 9, 2023, 12:46:15 PM

[rayman2000]

If I do the same thing with a point to the struct instead of the struct itself everything is fine.