Symbol tables are different when using the stainless command-line and the test suite

[jad-hamza]

Follow-up of: https://github.com/epfl-lara/inox/issues/80

At the moment this would be difficult to reproduce. If needed I can try at a later time.

[jad-hamza]

We can reproduce like this. If you have two independent files (2 and 3), which both depend on a file (File1), then in the tests, the trait A will contain both B and C as subclasses, which can slow down the verification. But from the command-line we only provide Stainless two files at a time (File1 and File2, or File1 and File3), making the verification tractable.

So there is no bug, it's normal behavior. Maybe something could be improved here, for instance by simplifying away classes that are not relevant for a VC, but we can close for now.

File1

object SymbolTable {
  trait A
}

File2

import SymbolTable._

object SymbolTable2 {
  case class B() extends A
}

File3

import SymbolTable._

object SymbolTable3 {
  case class C() extends A
}

[jad-hamza]

With the latest changes, unused classes should now be properly simplified (to be tested by https://github.com/epfl-lara/stainless/issues/334).

[samarion]

I believe that we still have different symbols. They may not be causing any issues in our current examples but we should probably keep the issue open.