search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 51 forks source link

Exception in SMTLIBParser #6

Closed jad-hamza closed 7 years ago

jad-hamza commented 7 years ago

This file produces an exception when run with stainless-scalac (corresponding tip-session attached)

import stainless.collection._
import stainless.lang._
import stainless.annotation._

object Crash {

  @induct
  def falseTheorem(k: BigInt, domain: List[BigInt]) = {
    require(domain.contains(k))

    false

  } holds
}

crash.txt

samarion commented 7 years ago

Well, this is due to the Z3 binary interface using identifiers of the shape k!0, k!1, etc. to encode models for arrays (and sets, in this case). Your k input variable also gets translated to k!0 in the Z3 smtlib interface and we therefore have a collision...

I fixed the issue in the latest version of Inox but I won't bump the version for such a minor issue so this probably won't be available in stainless for a while. You can circumvent the issue either by using a different solver than smt-z3 or by avoiding the name k for your variables.