Skip to content

Fix 'unknown constant k0!xyz' arising in some cases when using smt-z3

Viktor Kuncak requested to merge github/fork/mario-bucev/smt-z3-iden-fix into scala-3.x

Created by: mario-bucev

The following snippet*:

object Test {

  sealed trait Term {
    def fun(b: BigInt): Boolean = this match {
      case Var(k) => k == b
    }
  }
  case class Var(k: BigInt) extends Term // Important! No crash occurs if the variable is named other than k


  def patmat(t: Term, b: BigInt): Unit = {
    t match {
      case Var(_) =>
        // Obviously not true, but we are interested in the unfolding of t.fun
        assert(t.fun(b))
        ()
    }
  }
}

triggers the following error when using smt-z3

error: Internal solver error in z3: line 47 column 75: unknown constant k0!0 (Term!2) 
warning:  - Result for 'body assertion' VC for patmat @16:16:
warning: !t.isInstanceOf[Var] || fun(t, b)
Test.scala:16:16: warning:  => UNKNOWN
                   assert(t.fun(b))

This tiny PR addresses this small issue.

*Issue found by Andrea Gilot and Noé De Santo with https://github.com/epfl-lara/bolts/blob/c77d1e6598b084fc12d67fbc991f743102dbcef4/system-f/Transformations.scala#L126

Merge request reports