Fatal error when comparing options of different types

[jad-hamza]

import stainless.lang._

object StainlessIssueOption {
  def tt[A, B](a: A, b: B): Boolean = Some(a) == Some(b)
}

I don't remember if this should be supported or not, but perhaps we can improve the reporting in this case

[ Fatal  ] Run has failed with error: inox.ast.Definitions$ADTLookupException: Lookup failed for adt with symbol `Option$3`
[ Fatal  ] 
[ Fatal  ] inox.ast.Definitions$AbstractSymbols.$anonfun$getConstructor$1(Definitions.scala:182)
[ Fatal  ] scala.Option.getOrElse(Option.scala:189)
[ Fatal  ] inox.ast.Definitions$AbstractSymbols.getConstructor(Definitions.scala:182)
[ Fatal  ] inox.ast.Definitions$AbstractSymbols.getConstructor$(Definitions.scala:181)
[ Fatal  ] inox.ast.SimpleSymbols$SimpleSymbols.getConstructor(SimpleSymbols.scala:12)
[ Fatal  ] inox.ast.DependencyGraph$SortCollector.traverse(DependencyGraph.scala:23)
[ Fatal  ] inox.ast.DependencyGraph$SortCollector.traverse$(DependencyGraph.scala:21)
[ Fatal  ] stainless.ast.DependencyGraph$$anon$2.stainless$ast$DependencyGraph$SortCollector$$super$traverse(Graphs.scala:63)
[ Fatal  ] stainless.ast.DependencyGraph$SortCollector.traverse(Graphs.scala:59)
[ Fatal  ] stainless.ast.DependencyGraph$SortCollector.traverse$(Graphs.scala:54)
[ Fatal  ] stainless.ast.DependencyGraph$$anon$2.traverse(Graphs.scala:63)
[ Fatal  ] inox.transformers.TreeTraverser.traverse(Traverser.scala:96)
[ Fatal  ] inox.transformers.TreeTraverser.traverse$(Traverser.scala:96)
[ Fatal  ] stainless.ast.DependencyGraph$$anon$2.traverse(Graphs.scala:63)
[ Fatal  ] stainless.ast.DependencyGraph$$anon$2.traverse(Graphs.scala:63)
[ Fatal  ] inox.transformers.Traverser.$anonfun$traverse$4(Traverser.scala:29)
[ Fatal  ] inox.transformers.Traverser.$anonfun$traverse$4$adapted(Traverser.scala:29)
[ Fatal  ] scala.collection.immutable.List.foreach(List.scala:392)
[ Fatal  ] inox.transformers.Traverser.traverse(Traverser.scala:29)
[ Fatal  ] inox.transformers.Traverser.traverse$(Traverser.scala:25)
[ Fatal  ] stainless.ast.DependencyGraph$$anon$2.stainless$transformers$Traverser$$super$traverse(Graphs.scala:63)
[ Fatal  ] stainless.transformers.Traverser.traverse(Traverser.scala:21)
[ Fatal  ] stainless.transformers.Traverser.traverse$(Traverser.scala:12)
[ Fatal  ] stainless.ast.DependencyGraph$$anon$2.inox$transformers$TreeTraverser$$super$traverse(Graphs.scala:63)
[ Fatal  ] inox.transformers.TreeTraverser.traverse(Traverser.scala:95)
[ Fatal  ] inox.transformers.TreeTraverser.traverse$(Traverser.scala:95)
[ Fatal  ] stainless.ast.DependencyGraph$$anon$2.inox$ast$DependencyGraph$SortCollector$$super$traverse(Graphs.scala:63)
[ Fatal  ] inox.ast.DependencyGraph$SortCollector.traverse(DependencyGraph.scala:26)
[ Fatal  ] inox.ast.DependencyGraph$SortCollector.traverse$(DependencyGraph.scala:21)
[...]

[vkuncak]

This should probably be rejected on the grounds of #265

[romac]

I am also seeing Lookup failed for adt with symbol 'Option' errors in #768, still unclear to me where those come from.