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 9fbc579493e74048377c29e620b945bb5da8961e 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.
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:I would have thought this bug was introduced by 9fbc579493e74048377c29e620b945bb5da8961e but I've tested it against an older commit and it went through as well.
Note that
smt-cvc4
andsmt-z3
provide a correct counter-example.