Unsoundness of no-inc:z3 involving class invariants

[mario-bucev]

The following odd-looking snippet sometimes goes through with --solvers="no-inc:smt-z3:z3 tactic.default_tactic=smt sat.euf=true" (a solver we sometimes use, see e.g. SortedArray) even though it should not:

import stainless.*
import stainless.lang.*
import stainless.proof.*
import stainless.collection.*

object Min {

  case class Wrapper(dummy: BigInt, data: Data)

  case class Data(dummy: BigInt, values: ListMap[Int, Int]) {
    require(values.contains(3) && values.contains(4))
  }

  def test(w: Wrapper, x: BigInt): Unit = {
    require(x >= 0)
    decreases(x)
    if (x == 0) {
      w match {
        case w@Wrapper(_, _) => check(w.data.values.contains(3))
      }
      ()
    } else {
      test(w, x - 1)
    }
  }.ensuring(_ => false)
}

I would have thought this bug was introduced by 9fbc579 but I've tested it against an older commit and it went through as well.

Note that smt-cvc4 and smt-z3 provide a correct counter-example.